diff options
| author | notin | 2008-06-10 18:24:52 +0000 |
|---|---|---|
| committer | notin | 2008-06-10 18:24:52 +0000 |
| commit | 813b9b40ce96c59f9e68b759c876a0ccbfdbf942 (patch) | |
| tree | 4aa53fc2a9592970f39531aedca342aaa7cec1bc | |
| parent | d4e696cb8145701356fb9993a8a97e970e83ff8c (diff) | |
2-3 petites modifs sur la doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11091 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.doc | 6 | ||||
| -rwxr-xr-x | configure | 2 | ||||
| -rwxr-xr-x | doc/stdlib/Library.tex | 2 | ||||
| -rwxr-xr-x | doc/tutorial/Tutorial.tex | 8 |
4 files changed, 9 insertions, 9 deletions
diff --git a/Makefile.doc b/Makefile.doc index 3822fc7fb9..765aa18454 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -116,10 +116,10 @@ doc/refman-quick: doc/tutorial/Tutorial.v.dvi: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex (cd doc/tutorial; $(LATEX) Tutorial.v) -doc/tutorial/Tutorial.v.pdf: doc/common/version.tex doc/common/title.tex doc/tutorial/Tutorial.v.dvi +doc/tutorial/Tutorial.v.pdf: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex (cd doc/tutorial; $(PDFLATEX) Tutorial.v.tex) -doc/tutorial/Tutorial.v.html: doc/tutorial/Tutorial.v.tex +doc/tutorial/Tutorial.v.html: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex (cd doc/tutorial; hevea -exec xxdate.exe Tutorial.v) @@ -205,7 +205,7 @@ doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex # Not robust, improve... ide/index_urls.txt: doc/refman/html/index.html - rm ide/index_urls.txt - cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-itemize | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > ide/index_urls.txt + cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > ide/index_urls.txt ###################################################################### @@ -7,7 +7,7 @@ ################################## VERSION=trunk -DATE="Oct. 2007" +DATE="Jun. 2008" # a local which command for sh which () { diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 9260e7e189..8735bc720f 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,7 +3,7 @@ \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} -\usepackage{coqdoc} +\usepackage{../../coqdoc} \input{../common/version} \input{../common/title} diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 6e913e7319..cbe130a60d 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -59,7 +59,7 @@ invocation of \Coq\ delivers a message such as: \begin{flushleft} \begin{verbatim} unix:~> coqtop -Welcome to Coq 8.0 (Mar 2004) +Welcome to Coq trunk (Jun. 2008) Coq < \end{verbatim} @@ -67,9 +67,9 @@ Coq < \end{small} The first line gives a banner stating the precise version of \Coq~ -used. You should always return this banner when you report an -anomaly to our hot-line \verb:coq-bugs@pauillac.inria.fr: or on our -bug-tracking system~:\verb|http://logical.futurs.inria.fr/coq-bugs| +used. You should always return this banner when you report an anomaly +to our bug-tracking system +\verb|http://logical.futurs.inria.fr/coq-bugs| \chapter{Basic Predicate Calculus} |