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

3 files changed, 16 insertions, 10 deletions

diff --git a/Makefile.build b/Makefile.build
index a90eb0eb99..74845263c9 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -637,12 +637,12 @@ install-binaries:: install-$(BEST) install-tools
 
 install-byte::
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CSDPCERT) $(FULLBINDIR)
 	cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE)
 
 install-opt::
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CSDPCERT) $(FULLBINDIR)
 	cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE)
 
 install-tools::
@@ -866,7 +866,7 @@ endif
 
 %.ml: %.mll
 	$(SHOW)'OCAMLLEX  $<'
-	$(HIDE)$(OCAMLLEX) "$*.mll" -o $@
+	$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
 
 %.ml %.mli: %.mly
 	$(SHOW)'OCAMLYACC $<'
diff --git a/Makefile.common b/Makefile.common
index 915f383e0c..b58032077e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -877,7 +877,7 @@ VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
   setoids sorting natural integer rational numbers noreal \
   omega micromega ring setoid_ring dp xml extraction field fourier jprover \
   funind cc programs subtac rtauto
-DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial
+DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep
 STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \
   coqlight states pcoq-files check init theories theories-light contrib \
   $(DOC_TARGETS) $(VO_TARGETS)
diff --git a/Makefile.doc b/Makefile.doc
index 55d5d77ce7..241ba8bc47 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) >> $@