From 6bae2b22d2280bf25685f8bea5e94fe766d136fa Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 10 Mar 2000 17:48:49 +0000
Subject: compilation theories/Arith

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 38588d38ad..b3e8af9bd4 100644
--- a/Makefile
+++ b/Makefile
@@ -41,7 +41,7 @@ OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
 CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE)
 
-COQINCLUDES=-I theories/Init -I theories/Logic
+COQINCLUDES=-I theories/Init -I theories/Logic -I theories/Arith
 
 ###########################################################################
 # Objects files 
@@ -211,13 +211,24 @@ clean::
 
 LOGICVO=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/Eqdep_dec.vo      \
-      theories/Logic/Classical_Prop.vo
-
-theories/Logic/%.vo: theories/Logic/%.v states/initial.coq
-	$(COQC) -q -I theories/Init $<
-
-theories: $(INITVO) $(LOGICVO)
+      theories/Logic/Classical_Pred_Type.vo  theories/Logic/Classical_Prop.vo
+#     theories/Logic/Eqdep_dec.vo      \
+      
+ARITHVO=theories/Arith/Arith.vo         theories/Arith/Gt.vo          \
+	theories/Arith/Between.vo       theories/Arith/Le.vo          \
+	theories/Arith/Compare.vo       theories/Arith/Lt.vo          \
+	theories/Arith/Compare_dec.vo   theories/Arith/Min.vo         \
+	theories/Arith/Div.vo           theories/Arith/Minus.vo       \
+	theories/Arith/Div2.vo          theories/Arith/Mult.vo        \
+	theories/Arith/EqNat.vo         theories/Arith/Peano_dec.vo   \
+	theories/Arith/Euclid_def.vo    theories/Arith/Plus.vo        \
+	theories/Arith/Euclid_proof.vo  theories/Arith/Wf_nat.vo      \
+	theories/Arith/Even.vo
+
+#theories/Logic/%.vo: theories/Logic/%.v states/initial.coq
+#	$(COQC) -q -I theories/Init $<
+
+theories: $(INITVO) $(LOGICVO) $(ARITHVO)
 
 clean::
 	rm -f theories/*/*.vo theories/*/*~
-- 
cgit v1.2.3