From c1466b54d098e4e410aefacd6317bf8fa40bb63c Mon Sep 17 00:00:00 2001 From: mohring Date: Tue, 6 Jan 2004 16:52:44 +0000 Subject: doc avec frames git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8469 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/Makefile | 10 +++++----- doc/Reference-Manual.tex | 10 ++++++++++ doc/cover.html | 12 +++--------- doc/macros.tex | 4 ++++ doc/main-0.html | 29 +++++++++++++++++++++++++++++ doc/main.html | 13 +++++++++++++ doc/title.tex | 5 +++-- 7 files changed, 67 insertions(+), 16 deletions(-) create mode 100644 doc/main-0.html create mode 100644 doc/main.html diff --git a/doc/Makefile b/doc/Makefile index f330cdc6a7..ede88a11d7 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -154,8 +154,8 @@ doc-html.tar.gz: all-html rm -rf coq-docs-html/* cp Tutorial.v.html coq-docs-html/tutorial.html cp Reference-Manual.html coqide-queries.png coqide.png coq-docs-html - (cd coq-docs-html; hacha ./Reference-Manual.html; rm ./Reference-Manual.html) - cp cover.html coq-docs-html + (cd coq-docs-html; hacha -o toc.html ./Reference-Manual.html; rm ./Reference-Manual.html) + cp cover.html main.html main-0.html coq-docs-html tar cf doc-html.tar coq-docs-html gzip -f doc-html.tar @@ -164,9 +164,9 @@ html-www: all-html - $(MKDIR) www rm -rf www/* cp Tutorial.v.html www/tutorial.html - cp Reference-Manual.html coqide-queries.png coqide.png www - (cd www; hacha ./Reference-Manual.html; rm ./Reference-Manual.html) - cp cover.html www + cp coqide-queries.png coqide.png www + (cd www; hacha -o toc.html ../Reference-Manual.html) + cp cover.html main.html main-0.html www clean-refman: diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index 2e6c458439..0b9a8cc255 100644 --- a/doc/Reference-Manual.tex +++ b/doc/Reference-Manual.tex @@ -10,6 +10,7 @@ \usepackage{verbatim} \usepackage{amsmath} \usepackage{amssymb} +\usepackage{hevea} % for coqide \ifx\pdfoutput\undefined % si on est pas en pdflatex @@ -32,13 +33,17 @@ %END LATEX \tophtml{} +%BEGIN LATEX \coverpage{Reference Manual}{The Coq Development Team} +%END LATEX %\defaultheaders \include{RefMan-int}% Introduction \include{RefMan-pre}% Credits +%BEGIN LATEX \tableofcontents +%END LATEX \part{The language} \defaultheaders @@ -85,14 +90,19 @@ \nocite{*} \bibliographystyle{plain} \bibliography{biblio} +\cutname{biblio.html} \printindex +\cutname{general-index.html} \printindex[tactic] +\cutname{tactic-index.html} \printindex[command] +\cutname{command-index.html} \printindex[error] +\cutname{error-index.html} %BEGIN LATEX \listoffigures diff --git a/doc/cover.html b/doc/cover.html index 56063de895..792f1129be 100644 --- a/doc/cover.html +++ b/doc/cover.html @@ -1,17 +1,11 @@ - Cover Page - - - - -
@@ -20,7 +14,7 @@ The Coq Proof Assistant

Reference Manual


Version 8.0 -1










+1










The Coq Development Team
LogiCal Project













@@ -30,8 +24,8 @@ The Coq Proof Assistant


ŠINRIA 1999-2003

- - +
1
This research was partly supported by IST working group ``Types'' +
diff --git a/doc/macros.tex b/doc/macros.tex index 02dd1baefe..e385381cd1 100755 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -6,6 +6,10 @@ %\newcommand{\com}[1]{{\it(* #1 *)}} %\newcommand{\com}[1]{} +%%OPTIONS for HACHA +%\renewcommand{\cuttingunit}{section} + + %BEGIN LATEX \newenvironment{centerframe}% {\bgroup diff --git a/doc/main-0.html b/doc/main-0.html new file mode 100644 index 0000000000..db19678f3c --- /dev/null +++ b/doc/main-0.html @@ -0,0 +1,29 @@ + + + + +
+ + + + + + + + + + +
Cover page
Table of contents
+Bibliography
+Global Index +
+Tactics Index +
+Vernacular Commands Index +
+Index of Error Messages +
+ +
+ + \ No newline at end of file diff --git a/doc/main.html b/doc/main.html new file mode 100644 index 0000000000..1b5898298c --- /dev/null +++ b/doc/main.html @@ -0,0 +1,13 @@ + + + + +The Coq Proof Assistant Reference Manual + + + + + + + + \ No newline at end of file diff --git a/doc/title.tex b/doc/title.tex index 53ad9e0f89..d332af0577 100755 --- a/doc/title.tex +++ b/doc/title.tex @@ -41,16 +41,16 @@ The Coq Proof Assistant\\ {\Large \bf LogiCal Project}\\ \vspace{15pt} \end{center} - %BEGIN LATEX \newpage \vspace*{520pt} \thispagestyle{empty} %END LATEX - \begin{flushleft} +%BEGIN LATEX {\large{V\coqversion, \printingdate}}\\[20pt] +%END LATEX {\large{\copyright INRIA 1999-2004}}\\ \end{flushleft} %BEGIN LATEX @@ -58,6 +58,7 @@ The Coq Proof Assistant\\ %END LATEX } + \newcommand{\shorttitle}[1]{ \begin{center} \begin{huge} -- cgit v1.2.3