diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-10 17:15:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-10 17:15:38 +0000 |
| commit | c40522d74f33aaf69ebe172e93341332f8524b86 (patch) | |
| tree | 5ea4da9a6835d7ae7c799d8e0ed8b20c612f3287 /Makefile | |
| parent | 36714dadfbc9f8ba84f8f5f247b503fbf80e3d3a (diff) | |
Ajout ClassicalFacts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3113 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -441,6 +441,7 @@ LOGICVO=theories/Logic/Hurkens.vo theories/Logic/ProofIrrelevance.vo\ theories/Logic/Classical.vo theories/Logic/Classical_Type.vo \ theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo \ theories/Logic/Classical_Pred_Type.vo theories/Logic/Classical_Prop.vo \ + theories/Logic/ClassicalFacts.vo \ theories/Logic/Berardi.vo theories/Logic/Eqdep_dec.vo \ theories/Logic/Decidable.vo theories/Logic/JMeq.vo @@ -604,7 +605,9 @@ FIELDVO = contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo \ XMLVO = Xml.vo -INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/vernacrc +INTERFACEV0 = contrib/interface/Centaur.vo + +INTERFACERC = contrib/interface/vernacrc FOURIERVO = contrib/fourier/Fourier_util.vo contrib/fourier/Fourier.vo @@ -624,7 +627,7 @@ CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ $(CONTRIBVO): states/initial.coq -contrib: $(CONTRIBVO) $(CONTRIBCMO) +contrib: $(CONTRIBVO) $(CONTRIBCMO) $(INTERFACERC) omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) ring: $(RINGVO) $(RINGCMO) # xml_ instead of xml to avoid conflict with "make xml" |