diff options
| author | filliatr | 2000-03-16 22:47:33 +0000 |
|---|---|---|
| committer | filliatr | 2000-03-16 22:47:33 +0000 |
| commit | 2f15f87ee19c3e1a99765aa4b38e0d04731dfc3b (patch) | |
| tree | 9a572b879b917e3f7d8c21f651f57d53beda6c7c | |
| parent | 93da0ad0e56bf54f1be8913d0a5832868fc6be7c (diff) | |
theories/Bool
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@319 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile | 14 |
1 files changed, 10 insertions, 4 deletions
@@ -41,7 +41,8 @@ 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 -I theories/Arith +COQINCLUDES=-I theories/Init -I theories/Logic -I theories/Arith \ + -I theories/Bool ########################################################################### # Objects files @@ -225,10 +226,15 @@ ARITHVO=theories/Arith/Arith.vo theories/Arith/Gt.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 $< +BOOLVO=theories/Bool/Bool.vo theories/Bool/IfProp.vo \ + theories/Bool/Zerob.vo theories/Bool/DecBool.vo theories/Bool/Sumbool.vo -theories: $(INITVO) $(LOGICVO) $(ARITHVO) +theories: $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) + +init: $(INITVO) +logic: $(LOGICVO) +arith: $(ARITHVO) +bool: $(BOOLVO) clean:: rm -f theories/*/*.vo theories/*/*~ |