diff options
| author | filliatr | 1999-12-13 09:07:25 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-13 09:07:25 +0000 |
| commit | 677cf7db31c0dbf2f138ba2d25063737dfc662c5 (patch) | |
| tree | 31ed7936e2db7c1d72665e23a61e030434e686f8 /Makefile | |
| parent | e23a63f9920eff0fcc392dcdf11806393402d24c (diff) | |
documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 21 |
1 files changed, 19 insertions, 2 deletions
@@ -122,7 +122,7 @@ CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx) COQMKTOP=scripts/coqmktop COQC=scripts/coqc -world: $(COQMKTOP) $(COQC) coqtop.byte coqtop.opt states tools +world: $(COQMKTOP) $(COQC) coqtop.byte coqtop.opt states theories tools coqtop.opt: $(COQMKTOP) $(CMX) $(COQMKTOP) -opt -notactics $(OPTFLAGS) -o coqtop.opt @@ -183,6 +183,19 @@ states/barestate.coq: $(SYNTAXPP) coqtop.byte ./coqtop.byte -q -batch -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq ########################################################################### +# theories +########################################################################### + +INIT=theories/Init/Datatypes.vo theories/Init/Peano.vo \ + theories/Init/DatatypesSyntax.vo theories/Init/Prelude.vo \ + theories/Init/Logic.vo theories/Init/Specif.vo \ + theories/Init/LogicSyntax.vo theories/Init/SpecifSyntax.vo \ + theories/Init/Logic_Type.vo theories/Init/Wf.vo \ + theories/Init/Logic_TypeSyntax.vo + +theories: $(INIT) + +########################################################################### # tools ########################################################################### @@ -416,11 +429,14 @@ cleanconfig:: # Dependencies ########################################################################### -alldepend: depend dependcamlp4 +alldepend: depend dependcoq dependcamlp4 depend: beforedepend $(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend +dependcoq: beforedepend + tools/coqdep $(COQINCLUDES) */*.v */*/*.v > .depend.coq + dependcamlp4: beforedepend rm -f .depend.camlp4 for f in */*.ml4; do \ @@ -431,4 +447,5 @@ dependcamlp4: beforedepend done include .depend +include .depend.coq include .depend.camlp4 |