From c40522d74f33aaf69ebe172e93341332f8524b86 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 10 Oct 2002 17:15:38 +0000
Subject: Ajout ClassicalFacts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3113 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 .depend.coq | 1 +
 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
diff --git a/Makefile b/Makefile
index 32b8315963..8a92ad2b4d 100644
--- a/Makefile
+++ b/Makefile
@@ -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"
-- 
cgit v1.2.3