GitHub - tabareau/Forcing: Forcing layer on top of Coq

tabareau / Forcing Public

forked from mattam82/Forcing

Notifications You must be signed in to change notification settings
Fork 0
Star 1

Forcing layer on top of Coq

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 88 Commits
src		src
test-suite		test-suite
theories		theories
Make		Make
README		README

Repository files navigation

Forcing layer on top of Coq - copyright (c) 2012 Matthieu Sozeau <[email protected]>

Do coq_makefile -f Make -o Makefile
Compile, add to your ~/.coqrc:

Add ML Path "SOMEPATH/Forcing/src".
Add Rec LoadPath "SOMEPATH/Forcing/theories" as Forcing.

Enjoy!