diff options
| -rw-r--r-- | .depend.coq | 1 | ||||
| -rw-r--r-- | Makefile | 7 |
2 files changed, 6 insertions, 2 deletions
diff --git a/.depend.coq b/.depend.coq index 54d0a151d7..7b615e8ad0 100644 --- a/.depend.coq +++ b/.depend.coq @@ -184,6 +184,7 @@ theories/Logic/JMeq.vo: theories/Logic/JMeq.v theories/Logic/Decidable.vo: theories/Logic/Decidable.v theories/Logic/Eqdep_dec.vo: theories/Logic/Eqdep_dec.v theories/Logic/Berardi.vo: theories/Logic/Berardi.v +theories/Logic/ClassicalFacts.vo: theories/Logic/ClassicalFacts.v theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v theories/Logic/ProofIrrelevance.vo theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Eqdep.vo: theories/Logic/Eqdep.v @@ -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" |