aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-16 14:54:53 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-16 14:54:53 +0000
commitcc1eab7783dfcbc6ed088231109553ec51eccc3f (patch)
tree80757882fc1a6f30541a5c79c9c76c9e94315fbc /Makefile.doc
parentcf57e0cdafd45cf6944666086ec14174705f0b61 (diff)
Ajout de cibles pour le manuel de référence (refman-nodep, stdlib-nodep, refman-quick)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11229 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.doc')
-rw-r--r--Makefile.doc18
1 files changed, 12 insertions, 6 deletions
diff --git a/Makefile.doc b/Makefile.doc
index 55d5d77ce..241ba8bc4 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -27,13 +27,19 @@ doc-ps:\
doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \
doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.v.ps
-refman:\
+refman: coq
+ $(MAKE) -f Makefile.stage3 refman-nodep
+
+refman-nodep:\
doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf
tutorial:\
doc/tutorial/Tutorial.v.html doc/tutorial/Tutorial.v.ps doc/tutorial/Tutorial.v.pdf
-stdlib:\
+stdlib: $(THEORIESVO) $(COQDOC)
+ $(MAKE) -f Makefile.stage3 stdlib-nodep
+
+stdlib-nodep:\
doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf
faq:\
@@ -47,7 +53,7 @@ rectutorial:\
### Implicit rules
######################################################################
-%.v.tex: %.tex coq
+%.v.tex: %.tex
(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
%.ps: %.dvi
@@ -103,7 +109,7 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
$(INSTALLLIB) doc/refman/cover.html doc/refman/menu.html doc/refman/html
$(INSTALLLIB) doc/refman/index.html doc/refman/html
-doc/refman-quick:
+refman-quick:
(cd doc/refman; \
$(PDFLATEX) Reference-Manual.tex; \
$(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex)
@@ -152,7 +158,7 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
### Standard library (browsable html format)
-doc/stdlib/index-body.html: $(THEORIESVO:.vo=.glob) $(COQDOC)
+doc/stdlib/index-body.html:
- rm -rf doc/stdlib/html
$(MKDIR) doc/stdlib/html
$(COQDOC) -q -d doc/stdlib/html --multi-index --html \
@@ -169,7 +175,7 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm
### Standard library (light version, full version is definitely too big)
-doc/stdlib/Library.coqdoc.tex: $(THEORIESLIGHTVO:.vo=.glob) $(COQDOC)
+doc/stdlib/Library.coqdoc.tex:
$(COQSRC)/$(COQDOC) -q --gallina --body-only --latex --stdout \
-R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@