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

Branches Tags

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 <matthieu.sozeau@inria.fr>

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!