From 3394cf3ee974d3de4f9da6cba567d81ec372466a Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 27 Jan 2009 14:02:22 +0000 Subject: - Fixed various Overfull in documentation. - Removed useless coq-tex preprocessing of RecTutorial. - Make "Set Printing Width" applies to "Show Script" too. - Completed documentation (specially of ltac) according to CHANGES file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.doc | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) (limited to 'Makefile.doc') diff --git a/Makefile.doc b/Makefile.doc index 5afd12393..9382e1b6f 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -17,15 +17,15 @@ doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt doc-html:\ doc/tutorial/Tutorial.v.html doc/refman/html/index.html \ - doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.v.html + doc/faq/html/index.html doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.html doc-pdf:\ doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \ - doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.v.pdf + doc/faq/FAQ.v.pdf doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.pdf 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 + doc/faq/FAQ.v.ps doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps refman: \ doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf @@ -38,8 +38,8 @@ stdlib: \ faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf -rectutorial: doc/RecTutorial/RecTutorial.v.html \ - doc/RecTutorial/RecTutorial.v.ps doc/RecTutorial/RecTutorial.v.pdf +rectutorial: doc/RecTutorial/RecTutorial.html \ + doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf ###################################################################### ### Implicit rules @@ -216,32 +216,32 @@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li (cd doc/stdlib;\ $(LATEX) -interaction=batchmode Library;\ $(LATEX) -interaction=batchmode Library > /dev/null;\ - ../tools/show_latex_messages Library.log) + ../tools/show_latex_messages -no-overfull Library.log) doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi (cd doc/stdlib;\ $(PDFLATEX) -interaction=batchmode Library;\ - ../tools/show_latex_messages Library.log) + ../tools/show_latex_messages -no-overfull Library.log) ###################################################################### # Tutorial on inductive types ###################################################################### -doc/RecTutorial/RecTutorial.v.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.tex +doc/RecTutorial/RecTutorial.dvi: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.tex (cd doc/RecTutorial;\ - $(LATEX) -interaction=batchmode RecTutorial.v;\ - $(BIBTEX) -terse RecTutorial.v;\ - $(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\ - $(LATEX) -interaction=batchmode RecTutorial.v > /dev/null;\ - ../tools/show_latex_messages RecTutorial.v.log) + $(LATEX) -interaction=batchmode RecTutorial;\ + $(BIBTEX) -terse RecTutorial;\ + $(LATEX) -interaction=batchmode RecTutorial > /dev/null;\ + $(LATEX) -interaction=batchmode RecTutorial > /dev/null;\ + ../tools/show_latex_messages RecTutorial.log) -doc/RecTutorial/RecTutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.v.dvi +doc/RecTutorial/RecTutorial.pdf: doc/common/version.tex doc/common/title.tex doc/RecTutorial/RecTutorial.dvi (cd doc/RecTutorial;\ - $(PDFLATEX) -interaction=batchmode RecTutorial.v.tex;\ - ../tools/show_latex_messages RecTutorial.v.log) + $(PDFLATEX) -interaction=batchmode RecTutorial.tex;\ + ../tools/show_latex_messages RecTutorial.log) -doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex - (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial.v) +doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex + (cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial) ###################################################################### # Index file for CoqIDE @@ -267,7 +267,7 @@ install-doc-html: $(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq) $(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib - $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.html $(FULLDOCDIR)/html/RecTutorial.html + $(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html $(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq $(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html @@ -278,8 +278,8 @@ install-doc-printable: $(INSTALLLIB) doc/refman/Reference-Manual.ps \ doc/stdlib/Library.ps $(FULLDOCDIR)/ps $(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf - $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf + $(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf $(INSTALLLIB) doc/faq/FAQ.v.pdf $(FULLDOCDIR)/pdf/FAQ.pdf $(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps - $(INSTALLLIB) doc/RecTutorial/RecTutorial.v.ps $(FULLDOCDIR)/ps/RecTutorial.ps + $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps $(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps -- cgit v1.2.3