Fusion des fichiers de syntaxe de Init avec les fichiers de définition; TypeSyntax inutile

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 3 deletions

diff --git a/Makefile b/Makefile
index a8e4d4f97..805ed5647 100644
--- a/Makefile
+++ b/Makefile
@@ -528,9 +528,8 @@ states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP)
 INITVO=theories/Init/Notations.vo \
        theories/Init/Datatypes.vo         theories/Init/Peano.vo         \
        theories/Init/Logic.vo             theories/Init/Specif.vo        \
-       theories/Init/LogicSyntax.vo       theories/Init/SpecifSyntax.vo  \
        theories/Init/Logic_Type.vo        theories/Init/Wf.vo            \
-       theories/Init/Logic_TypeSyntax.vo  theories/Init/Prelude.vo
+       theories/Init/Prelude.vo
 
 
 theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC)
@@ -635,7 +634,7 @@ WELLFOUNDEDVO=theories/Wellfounded/Disjoint_Union.vo \
 	      theories/Wellfounded/Well_Ordering.vo \
 	      theories/Wellfounded/Lexicographic_Product.vo 
 
-REALSBASEVO=theories/Reals/TypeSyntax.vo \
+REALSBASEVO=\
 	theories/Reals/Rdefinitions.vo theories/Reals/Rsyntax.vo \
 	theories/Reals/Raxioms.vo      theories/Reals/RIneq.vo \
 	theories/Reals/DiscrR.vo       theories/Reals/Rbase.vo \