diff options
| author | filliatr | 2000-03-10 17:48:49 +0000 |
|---|---|---|
| committer | filliatr | 2000-03-10 17:48:49 +0000 |
| commit | 6bae2b22d2280bf25685f8bea5e94fe766d136fa (patch) | |
| tree | 47ed8295ac663803396dfdfb6d0001f58ca959df /Makefile | |
| parent | 9f8ccadf2f68ff44ee81d782b6881b9cc3c04c4b (diff) | |
compilation theories/Arith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@312 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 27 |
1 files changed, 19 insertions, 8 deletions
@@ -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/*/*~ |