From 677cf7db31c0dbf2f138ba2d25063737dfc662c5 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 13 Dec 1999 09:07:25 +0000
Subject: documentation

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 974feb8b45..1242cbb244 100644
--- a/Makefile
+++ b/Makefile
@@ -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
@@ -182,6 +182,19 @@ SYNTAXPP=syntax/PPCommand.v syntax/PPTactic.v syntax/PPCases.v
 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
-- 
cgit v1.2.3