From 58b3bc4b3151bc5f8b81fbc7a1943f99b081f80e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 Sep 2003 11:23:14 +0000
Subject: 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
---
 Makefile | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index a8e4d4f973..805ed5647f 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 \
-- 
cgit v1.2.3