From b496630ec937dbf2d823d76c53cf6ab81b1544a9 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Mon, 24 Feb 2003 17:12:57 +0000
Subject: Bringing Linear back to life (Still somewhat buggy).

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 4ec92ca607..41b613d303 100644
--- a/Makefile
+++ b/Makefile
@@ -44,7 +44,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/jprover -I contrib/cc -I contrib/linear
 
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
@@ -347,11 +347,24 @@ JPROVERCMO=\
 
 CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo  
 
-ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4
+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=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-	$(CORRECTNESSCMO) $(CCCMO) $(USERCMO)
+	$(CORRECTNESSCMO) $(CCCMO) $(LINEARCMO) $(USERCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
-- 
cgit v1.2.3