From 8b5f6f835be01b2b0510cdbea939050d2c2583c6 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Thu, 16 Oct 2003 15:44:47 +0000
Subject: Ground update + Linear removal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4654 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 19 +++----------------
 1 file changed, 3 insertions(+), 16 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index e9f0e26fdd..be973fe596 100644
--- a/Makefile
+++ b/Makefile
@@ -61,7 +61,7 @@ LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
 	      -I contrib/ring -I contrib/xml \
 	      -I contrib/extraction -I contrib/correctness \
               -I contrib/interface -I contrib/fourier \
-	      -I contrib/jprover -I contrib/cc -I contrib/linear \
+	      -I contrib/jprover -I contrib/cc \
 	      -I contrib/funind -I contrib/first-order
 
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
@@ -301,25 +301,12 @@ FOCMO=\
 
 CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo  
 
-LINEARCMO=\
-  contrib/linear/dpctypes.cmo \
-  contrib/linear/general.cmo \
-  contrib/linear/graph.cmo \
-  contrib/linear/subst.cmo \
-  contrib/linear/unif.cmo \
-  contrib/linear/lk_proofs.cmo \
-  contrib/linear/ccidpc.cmo \
-  contrib/linear/kwc.cmo \
-  contrib/linear/prove.cmo \
-  contrib/linear/dpc.cmo
-
 ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \
-  contrib/linear/ccidpc.ml4 contrib/linear/dpc.ml4 contrib/funind/tacinv.ml4 \
-  contrib/first-order/g_ground.ml4
+  contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-	$(CORRECTNESSCMO) $(CCCMO) $(LINEARCMO) $(FUNINDCMO) $(FOCMO)
+	$(CORRECTNESSCMO) $(CCCMO) $(FUNINDCMO) $(FOCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
-- 
cgit v1.2.3