plus derreur hevea/hacha

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8471 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 32 insertions, 22 deletions

diff --git a/doc/Extraction.tex b/doc/Extraction.tex
index 19be945603..c315cdf78d 100755
--- a/doc/Extraction.tex
+++ b/doc/Extraction.tex
@@ -107,30 +107,34 @@ produce more readable code.
 All these optimizations are controled by the following \Coq\ options: 
 
 \begin{description}
-\comindex{Set Extraction Optimize}
-\comindex{Unset Extraction Optimize}
-\item {\tt Set Extraction Optimize.}
-\item {\tt Unset Extraction Optimize.} ~\par
+
+\item \comindex{Set Extraction Optimize}
+{\tt Set Extraction Optimize.}
+
+\item \comindex{Unset Extraction Optimize}
+{\tt Unset Extraction Optimize.}
 
 Default is Set. This control all optimizations made on the ML terms 
 (mostly reduction of dummy beta/iota redexes, but also simplications on 
 Cases, etc). Put this option to Unset if you want a ML term as close as 
 possible to the Coq term.
 
-\comindex{Set Extraction AutoInline}
-\comindex{Unset Extraction AutoInline}
-\item {\tt Set Extraction AutoInline.}
-\item {\tt Unset Extraction AutoInline.} ~\par
+\item \comindex{Set Extraction AutoInline}
+{\tt Set Extraction AutoInline.} 
+
+\item \comindex{Unset Extraction AutoInline}
+{\tt Unset Extraction AutoInline.} 
 
 Default is Set, so by default, the extraction mechanism feels free to 
 inline the bodies of some defined constants, according to some heuristics 
 like size of bodies, useness of some arguments, etc. Those heuristics are 
 not always perfect, you may want to disable this feature, do it by Unset. 
 
-\comindex{Extraction Inline}
-\comindex{Extraction NoInline}
-\item {\tt Extraction Inline} \qualid$_1$ \dots\ \qualid$_n$. ~\par 
-\item {\tt Extraction NoInline} \qualid$_1$ \dots\ \qualid$_n$. ~\par
+\item \comindex{Extraction Inline}
+{\tt Extraction Inline} \qualid$_1$ \dots\ \qualid$_n$. 
+
+\item \comindex{Extraction NoInline}
+{\tt Extraction NoInline} \qualid$_1$ \dots\ \qualid$_n$. 
 
 In addition to the automatic inline feature, you can now tell precisely to 
 inline some more constants by the {\tt Extraction Inline} command. Conversely, 
@@ -138,14 +142,14 @@ you can forbid the automatic inlining of some specific constants by
 the {\tt Extraction NoInline} command.
 Those two commands enable a precise control of what is inlined and what is not. 
 
-\comindex{Print Extraction Inline}
-\item {\tt Print Extraction Inline}. ~\par
+\item \comindex{Print Extraction Inline}
+{\tt Print Extraction Inline}. 
 
 Prints the current state of the table recording the custom inlinings 
 declared by the two previous commands. 
 
-\comindex{Reset Extraction Inline}
-\item {\tt Reset Extraction Inline}. ~\par
+\item \comindex{Reset Extraction Inline}
+{\tt Reset Extraction Inline}. 
 
 Puts the table recording the custom inlinings back to empty. 
 
diff --git a/doc/Makefile b/doc/Makefile
index ede88a11d7..f338e3f57d 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -150,7 +150,7 @@ coq.info: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
 	hevea -info ./book-html.sty ./coq-html.sty ./Reference-Manual.tex
 
 doc-html.tar.gz: all-html
-	- $(MKDIR) coq-docs-html
+	$(MKDIR) -p coq-docs-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 
@@ -161,7 +161,7 @@ doc-html.tar.gz: all-html
 
 # Pour le site de Coq.
 html-www: all-html
-	- $(MKDIR) www
+	$(MKDIR) -p www
 	rm -rf www/*
 	cp Tutorial.v.html www/tutorial.html
 	cp coqide-queries.png coqide.png www
diff --git a/doc/headers.tex b/doc/headers.tex
index c7e46ef5cb..21b3b6e851 100644
--- a/doc/headers.tex
+++ b/doc/headers.tex
@@ -26,14 +26,13 @@
 \renewcommand{\bibname}{\protect\setheaders{Bibliography}%
 \protect\RefManCutCommand{BEGINBIBLIO=\thepage}%
 \protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography}
-%ENDLATEX
+%END LATEX
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % For the Addendum table of contents
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\makeatletter
-
 \newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip \bigskip \bigskip}
+\makeatletter
 %BEGIN LATEX
 \newcommand{\atableofcontents}{\section*{Contents}\@starttoc{atoc}}
 \newcommand{\achapter}[1]{
diff --git a/doc/macros.tex b/doc/macros.tex
index e385381cd1..b16c4fb095 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -26,7 +26,14 @@
 %END LATEX
 %HEVEA \newenvironment{centerframe}{\begin{center}}{\end{center}}
 
-%HEVEA \newcommand{\vec}[1]{\textbf{#1}}
+%HEVEA \newcommand{\vec}[1]{\mathbf{#1}}
+%HEVEA \newcommand{\ominus}{-}
+%HEVEA \renewcommand{\oplus}{+}
+%HEVEA \renewcommand{\otimes}{\times}
+%HEVEA \newcommand{\land}{\wedge}
+%HEVEA \newcommand{\lor}{\vee}
+%HEVEA \newcommand{\k}[1]{#1}
+%HEVEA \newcommand{\phantom}[1]{\qquad}
 
 %%%%%%%%%%%%%%%%%%%%%%%
 % Formatting commands %