tabareau/Forcing
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
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!