diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-05 21:57:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-05 21:57:47 +0000 |
| commit | 41b6404a15dafcf700addd0ce85ddd70cedb0219 (patch) | |
| tree | 2cc4945d5eefa6afee5b49cdfb2c4356f4d81202 /Makefile | |
| parent | 14644b3968658a30dffd6aa5d45f2765b5e6e72f (diff) | |
Modularisation des preuves concernant la logique classique, l'indiscernabilité des preuves et l'axiome K
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8136 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 5 |
1 files changed, 3 insertions, 2 deletions
@@ -137,7 +137,7 @@ LIBRARY=\ library/nameops.cmo library/libnames.cmo library/libobject.cmo \ library/summary.cmo library/nametab.cmo library/global.cmo library/lib.cmo \ library/declaremods.cmo library/library.cmo library/states.cmo \ - library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo + library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo PRETYPING=\ pretyping/termops.cmo pretyping/evd.cmo \ @@ -790,7 +790,8 @@ LOGICVO=\ theories/Logic/Berardi.vo theories/Logic/Eqdep_dec.vo \ theories/Logic/Decidable.vo theories/Logic/JMeq.vo \ theories/Logic/ClassicalDescription.vo theories/Logic/ClassicalChoice.vo \ - theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo + theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo \ + theories/Logic/EqdepFacts.vo theories/Logic/ProofIrrelevanceFacts.vo ARITHVO=\ theories/Arith/Arith.vo theories/Arith/Gt.vo \ |