ajout d'une passe de latex our avoir un index correct

+ quelques petites retouches sur la doc


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

15 files changed, 163 insertions, 143 deletions

diff --git a/doc/Cases.tex b/doc/Cases.tex
index a8ab494c77..95411afae9 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -349,13 +349,12 @@ Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
   | consn n' a y => consn (n' + m) a (concat n' y m l')
   end.
 \end{coq_example}
-The elimination predicate is $\lb n:\texttt{nat} \mto \lb
-l:(\texttt{listn}~ n) \mto (\texttt{listn}~ (n+m))$.
+The elimination predicate is {\tt fun (n:nat) (l:listn n) => listn~(n+m)}.
 In general if $m$ has type $(I~q_1\ldots q_r~t_1\ldots t_s)$ where 
 $q_1\ldots q_r$ are parameters, the elimination predicate should be of
 the form~:
-$\lb y_1\mto\ldots\lb y_s\mto \lb x:(I~q_1\ldots q_r~y_1\ldots y_s)
-P$. 
+{\tt fun $y_1$\ldots $y_s$ $x$:($I$~$q_1$\ldots $q_r$~$y_1$\ldots
+  $y_s$) => P}. 
 
 In the concrete syntax, it should be written~:
 \[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_\ldots \_~y_1\ldots y_s)~\kw{return}~Q~\kw{with}~\ldots~\kw{end}\]
@@ -401,12 +400,10 @@ correct Coq raises an error message. For example:
 \begin{coq_eval}
 Reset concat.
 Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(**** Error: The elimination predicate [n:nat](listn (plus n m))  ****)
-(*** should be of arity nat->nat->Type (for non dependent case) or ***)
-(** (n:nat)(listn n)->(n0:nat)(listn n0)->Type (for dependent case) **)
+(********** The following is not correct and should produce ***********)
+(** Error: the term l' has type listn m while it is expected to have **)
+(** type listn (?31 + ?32)                                           **)
 \end{coq_eval}
-
 \begin{coq_example}
 Fixpoint concat
  (n:nat) (l:listn n) (m:nat)
diff --git a/doc/Makefile b/doc/Makefile
index f338e3f57d..a0a50a6405 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -28,7 +28,7 @@ COQTOP=`$(DOCCOQC) -where`
 COQTEX=$(COQBINPATH)coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small
 #COQWEBSTY=$(HOME)/lib/tex/
 COQWEBSTY=/usr/share/texmf/tex/latex/misc/
-HEVEALIB=/usr/local/lib/hevea
+HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea
 
 LATEX=latex
 BIBTEX=bibtex -min-crossrefs=10
@@ -48,15 +48,16 @@ LIBFILES=library/Logic.tex library/Datatypes.tex library/Peano.tex \
 REFMANCOQTEXFILES=\
   RefMan-gal.v.tex RefMan-ext.v.tex RefMan-mod.v.tex RefMan-tac.v.tex \
   RefMan-cic.v.tex RefMan-lib.v.tex RefMan-tacex.v.tex \
-  RefMan-syn.v.tex RefMan-ltac.v.tex RefMan-oth.v.tex
+  RefMan-syn.v.tex RefMan-oth.v.tex
 
 COQTEXFILES= Cases.v.tex Coercion.v.tex Extraction.v.tex \
   Omega.v.tex Changes.v.tex Tutorial.v.tex Polynom.v.tex \
-  Correctness.v.tex Setoid.v.tex # Program.v.tex Natural.v.tex 
+  Setoid.v.tex
+#SUPPRIME: Program.v.tex Natural.v.tex Correctness.v.tex
 
 REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \
-  RefMan-pro.tex RefMan-com.tex RefMan-uti.tex RefMan-ide.tex \
-  coqide.eps coqide-queries.eps RefMan-add.tex RefMan-modr.tex \
+  RefMan-pro.tex RefMan-com.tex RefMan-ltac.tex RefMan-uti.tex \
+  RefMan-ide.tex coqide.eps coqide-queries.eps RefMan-add.tex RefMan-modr.tex \
   $(REFMANCOQTEXFILES) 
 
 REFMAN=Reference-Manual
@@ -292,9 +293,12 @@ Tutorial.v.pdf: ./version.tex ./title.tex Tutorial.v.tex
 
 Reference-Manual.ps: Reference-Manual.dvi
 
+# The second LATEX compilation is necessary otherwise the pages of the index
+# are not correct (don't know why...) - BB
 Reference-Manual.dvi: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
 	$(LATEX) Reference-Manual
 	$(BIBTEX) Reference-Manual
+	$(LATEX) Reference-Manual
 	$(MAKEINDEX) Reference-Manual
 	$(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind
 	$(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex
index 87b55744af..11672d633a 100755
--- a/doc/RefMan-cic.tex
+++ b/doc/RefMan-cic.tex
@@ -622,7 +622,7 @@ The declaration for the length of lists is:
 
 The declaration for a mutual inductive definition of forests and trees is:
 \[\NInd{}{\tree:\Set,\forest:\Set}
-      {\node:\forest \ra \tree,
+      {\\~~\node:\forest \ra \tree,
        \emptyf:\forest,\consf:\tree \ra \forest \ra \forest\-}\]
   
 These representations are the ones obtained as the result of the \Coq\ 
@@ -1179,7 +1179,7 @@ context being the same in all the judgments).
     {\Case{P}{l}{f_1~f_2}:(P~l)}\]
 
 \[\frac{
-     \begin{array}[b]{c} 
+     \begin{array}[b]{@{}c@{}} 
 H:(\LengthA~L~N) \\ P:\forall l:\ListA, \forall n:\nat, (\LengthA~l~n)\ra
   \Prop\\
  f_1:(P~(\Nil~A)~\nO~\LNil) \\
@@ -1363,9 +1363,13 @@ Definition sont (t:tree) : forest
    := let (f) := t in f.
 \end{coq_example}
 The following is not a conversion but can be proved after a case analysis.
+\begin{coq_eval}
+(******************************************************************)
+(** Error: Impossible to unify ....                              **)
+\end{coq_eval}
 \begin{coq_example}
 Goal forall t:tree, sizet t = S (sizef (sont t)).
-(** this one fails **) reflexivity.
+reflexivity. (** this one fails **)
 destruct t.
 reflexivity.
 \end{coq_example}
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 39541153de..ceacb39205 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -20,9 +20,10 @@ construction allows to define ``signatures''.
 \begin{tabular}{lcl}
 {\sentence} & ++= & {\record}\\
   & & \\
-{\record} & ::= &  {\tt Record} {\ident} \sequence{\binderlet}{} :
-  {\sort} := \zeroone{\ident} \{ \zeroone{\nelist{\field}{;}} 
-    \} . \\
+{\record} & ::= &
+   {\tt Record} {\ident} \sequence{\binderlet}{} {\tt :} {\sort} \verb.:=. \\
+&& ~~~~\zeroone{\ident}
+       \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\
   & & \\
 {\field} & ::= & {\name} : {\type} \\
  & $|$ & {\name} {\typecstr} := {\term}
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 083707469d..e856566c7b 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -228,10 +228,10 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\
  & $|$ & {\tt let cofix} {\cofixpointbody}
          {\tt in} {\term} &(\ref{fixpoints})\\
- & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} {\returntype}
+ & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} {\ifitem}
          {\tt :=} {\term}
          {\tt in} {\term}  &(\ref{caseanalysis}, \ref{Mult-match})\\
- & $|$ & {\tt if} {\ifitem} {\tt then} {\term}
+ & $|$ & {\tt if} {\term} {\ifitem} {\tt then} {\term}
          {\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\
  & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\
  & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\
@@ -251,8 +251,8 @@ chapter \ref{Addoc-syntax}.
 {\termarg} & ::= & {\term} &\\
  & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )}
          &(\ref{Implicits-explicitation})\\
- & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )}
-         &(\ref{Implicits-explicitation})\\
+%% & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )}
+%%         &(\ref{Implicits-explicitation})\\
 &&&\\
 {\binderlist} & ::= & \nelist{\name}{} {\typecstr} & \ref{Binders} \\
  & $|$ & {\binder} \nelist{\binderlet}{} &\\
@@ -531,8 +531,9 @@ annotation has to be given when the resulting type of the whole {\tt
 match} depends on the actual {\term$_0$} matched.
 
 There are specific notations for case analysis on types with one or
-two constructors: {\tt if}\ldots{\tt then}\ldots{\tt else}\ldots and
-{\tt let (}\ldots{\tt ) :=}\ldots{\tt in}\ldots. 
+two constructors: {\tt if / then / else} and
+{\tt let (}\ldots{\tt ) :=} \ldots {\tt in}\ldots. \SeeAlso
+section~\ref{Mult-match} for details and examples.
 
 \SeeAlso Section~\ref{Mult-match} for details and examples.
 
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 77b14dbd8d..5a022c74e5 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -145,8 +145,6 @@ First, we find propositional calculus connectives:
 
 \begin{coq_eval}
 Set Printing Depth 50.
-(********** Next parsing errors for /\ and \/ are harmless ***********)
-(******************* since output is not displayed *******************)
 \end{coq_eval}
 \begin{coq_example*}
 Inductive True : Prop := I.
@@ -200,9 +198,9 @@ The following abbreviations are allowed:
   \begin{tabular}[h]{|l|l|}
     \hline
     \verb+exists x:A, P+     & \verb+ex A (fun x:A => P)+ \\
-    \verb+exists x, P+       & \verb+ex A (fun x:A => P)+ \\
+    \verb+exists x, P+       & \verb+ex _ (fun x => P)+ \\
     \verb+exists2 x:A, P & Q+ & \verb+ex2 A (fun x:A => P) (fun x:A => Q)+ \\
-    \verb+exists2 x, P & Q+   & \verb+ex2 A (fun x:A => P) (fun x:A => Q)+ \\
+    \verb+exists2 x, P & Q+   & \verb+ex2 _ (fun x => P) (fun x => Q)+ \\
     \hline
   \end{tabular}
 \end{center}
diff --git a/doc/RefMan-modr.tex b/doc/RefMan-modr.tex
index 66895f204f..e7c8614c86 100644
--- a/doc/RefMan-modr.tex
+++ b/doc/RefMan-modr.tex
@@ -273,9 +273,9 @@ Specification subtyping rules:
 \inference{%
   \frac{
     \WTECONV{}{\Gamma_P}{\Gamma_P'}%
-    ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
-    ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
-    ~~~~~~~~\WTECONV{}{p}{p'}
+    ~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
+    ~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
+    ~~~~~~\WTECONV{}{p}{p'}
   }{
     \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
         {\Indp{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}{p'}}
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index 392d686583..60930ec06b 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -185,7 +185,10 @@ environment}\\
 
 \begin{Variants}
 \item {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{}
-].} where {\textrm{\textsl{qualid-or-string}}} is a {\qualid} or a {\str}.\\
+].}\\
+\noindent where {\textrm{\textsl{qualid-or-string}}} is a {\qualid} or
+a {\str}.
+
 This extension of {\tt SearchAbout} searches for all objects whose
 statement mentions all of {\qualid} of the list and whose name
 contains all {\str} of the list.
@@ -198,16 +201,21 @@ SearchAbout [ Zmult Zplus "distr" ].
 \end{coq_example}
 
 \item
-{\tt SearchAbout {\term} inside {\module$_1$} \ldots{} {\module$_n$}.}\\
-{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
-  inside {\module$_1$} \ldots{} {\module$_n$}.}
+\begin{tabular}[t]{@{}l}
+  {\tt SearchAbout {\term} inside {\module$_1$} \ldots{} {\module$_n$}.} \\
+  {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
+    inside {\module$_1$} \ldots{} {\module$_n$}.}
+\end{tabular}
 
 This restricts the search to constructions defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
-\item {\tt SearchAbout {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}\\
-{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
-  outside {\module$_1$} \ldots{} {\module$_n$}.}
+\item
+\begin{tabular}[t]{@{}l}
+  {\tt SearchAbout {\term} outside {\module$_1$}...{\module$_n$}.} \\
+  {\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ]
+     outside {\module$_1$}...{\module$_n$}.}
+\end{tabular}
 
 This restricts the search to constructions not defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
@@ -308,9 +316,10 @@ This restricts the search to constructions not defined in modules
 This command displays the full name of the qualified identifier {\qualid}
 and consequently the \Coq\ module in which it is defined.
 
-% (***************** The last line should produce **************************)
-% (************* Error: I.Dont.Exist not a defined object ******************)
-% (* Just to adjust the prompt: *) 
+\begin{coq_eval}
+(*************** The last line should produce **************************)
+(*********** Error: I.Dont.Exist not a defined object ******************)
+\end{coq_eval}
 \begin{coq_eval}
 Set Printing Depth 50.
 \end{coq_eval}
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 02e6f82784..a2132fb640 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -260,8 +260,8 @@ format} modifier. Here is an example
 \begin{small}
 \begin{coq_example}
 Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
- (at level 200, right associativity, format
-  "'[v   ' 'If'  c1 '/' '[' 'then'  c2  ']' '/' '[' 'else'  c3 ']' ']'").
+(at level 200, right associativity, format
+"'[v   ' 'If'  c1 '/' '[' 'then'  c2  ']' '/' '[' 'else'  c3 ']' ']'").
 \end{coq_example}
 \end{small}
 
@@ -770,6 +770,9 @@ expression. An abbreviation is a special form of notation with no
 parameter and only one symbol which is an identifier. This identifier
 is given with no quotes around. Example:
 
+\begin{coq_eval}
+Require Import List.
+\end{coq_eval}
 \begin{coq_example*}
 Notation List := (list nat).
 \end{coq_example*}
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 0b9f7b7b57..43c6f965b9 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1281,7 +1281,7 @@ Proof c.
 This tactic applies to any goal. If the variables {\ident$_1$} and
 {\ident$_2$} of the goal have an inductive type, then this tactic
 performs double induction on these variables.  For instance, if the
-current goal is \verb+(n,m:nat)(P n m)+ then, {\tt double induction n
+current goal is \verb+forall n m:nat, P n m+ then, {\tt double induction n
   m} yields the four cases with their respective inductive hypotheses.
 In particular the case for \verb+(P (S n) (S m))+ with the induction
 hypotheses \verb+(P (S n) m)+ and \verb+(m:nat)(P n m)+ (hence
@@ -1653,10 +1653,10 @@ introduced hypothesis.
 
 \item{\tt injection}\tacindex{injection} 
   
-  If the current goal is of the form {\tt
-    \verb=~={\term$_1$}={\term$_2$}}, the tactic computes the head
-  normal form of the goal and then behaves as the sequence: {\tt
-    unfold not; intro {\ident}; injection {\ident}}.
+  If the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$},
+  the tactic computes the head normal form of the goal and then
+  behaves as the sequence: {\tt unfold not; intro {\ident}; injection
+  {\ident}}.
   
   \ErrMsg \errindex{goal does not satisfy the expected preconditions}
 \end{Variants}
@@ -1678,7 +1678,8 @@ latter is first introduced in the local context using
 \texttt{intros until \ident}.
 
 \begin{Variants}
-\item \texttt{simplify\_eq} \num\\
+\item \texttt{simplify\_eq} \num
+
   This does the same thing as \texttt{intros until \num} then
 \texttt{simplify\_eq \ident} where {\ident} is the identifier for the last
 introduced hypothesis.
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index 95de3ca78b..a26a18267b 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -129,7 +129,6 @@ no value for {\tt y} in {\tt Rtrans} is found by {\tt apply}:
 Set Printing Depth 50.
 (********** The following is not correct and should produce **********)
 (**** Error: generated subgoal (R n ?17) has metavariables in it *****)
-(* Just to adjust the prompt: *) apply Rtrans.
 \end{coq_eval}
 \begin{coq_example}
 apply Rtrans.
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 0b9a8cc255..6199c68cf0 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -58,7 +58,7 @@
 \include{RefMan-oth.v}% Vernacular commands
 \include{RefMan-pro}% Proof handling
 \include{RefMan-tac.v}% Tactics and tacticals
-\include{RefMan-ltac.v}% Writing tactics
+\include{RefMan-ltac}% Writing tactics
 \include{RefMan-tacex.v}% Detailed Examples of tactics
 
 \part{User extensions}
diff --git a/doc/Translator.tex b/doc/Translator.tex
index 8e9f83bae0..005ca9c0c6 100644
--- a/doc/Translator.tex
+++ b/doc/Translator.tex
@@ -201,15 +201,15 @@ list_scope & \texttt{:: ++}
 \end{center}
 
 
+
 \subsubsection{Notation for implicit arguments}
 
 The explicitation of arguments is closer to the \emph{bindings}
 notation in tactics. Argument positions follow the argument names of
 the head constant. The example below assumes \verb+f+ is a function
-with two dependent arguments named \verb+x+ and \verb+y+, and a third
-non-dependent argument.
+with two implicit dependent arguments named \verb+x+ and \verb+y+.
 \begin{transbox}
-\TRANS{f 1!t1 2!t2 3!t3}{f (x:=t1) (y:=t2) (1:=t3)}
+\TRANS{f 1!t1 2!t2 t3}{f (x:=t1) (y:=t2) t3}
 \TRANS{!f t1 t2}{@f t1 t2}
 \end{transbox}
 
@@ -335,7 +335,7 @@ The same applies to cofixpoints, annotations are not allowed in that case.
 The main change is that all tactic names are lowercase. This also holds for
 Ltac keywords.
 
-\subsubsection{Renaming of tactics}
+\subsubsection{Renaming of induction tactics}
 
 \begin{transbox}
 \TRANS{NewDestruct}{destruct}
@@ -376,8 +376,8 @@ cases, when a \'{} was necessary, it is replaced by ``{\tt constr :}''
 {let x := constr:(fun x => S (S x)) in apply x}
 \end{transbox}
 
-{\tt Match Context} is now called {\tt match goal}. Its argument is an
-Ltac by default.
+{\tt Match Context With} is now called {\tt match goal with}. Its
+argument is an Ltac expression by default.
 
 
 \subsubsection{Named arguments of theorems ({\em bindings})}
@@ -400,9 +400,9 @@ the term itself and after keyword \TERM{as}.
 \subsubsection{{\tt LetTac} and {\tt Pose}}
 
 Tactic {\tt LetTac} was renamed into {\tt set}, and tactic {\tt Pose}
-was a particular case of {\tt LetTac}\footnote{There is a tactic
-called {\tt pose} in V8, but its behaviour is not to fold the
-abbreviation.}.
+was a particular case of {\tt LetTac} where the abbreviation is folded
+in the conclusion\footnote{There is a tactic called {\tt pose} in V8,
+but its behaviour is not to fold the abbreviation at all.}.
 
 \begin{transbox}
 \TRANS{LetTac x = t in H}{set (x := t) in H}
@@ -410,16 +410,16 @@ abbreviation.}.
 \end{transbox}
 
 {\tt LetTac} could be followed by a specification (called a clause) of
-the hypotheses where the abbreviation had to be folded (and also if it
-should occur in the conclusion). Clauses are the syntactic notion to
-denote in which parts of a goal a given transformation shold
-occur. Its basic notation is either \TERM{*} (meaning everywhere), or
-{\tt\textrm{\em hyps} |- \textrm{\em concl}} where {\em hyps} is
-either \TERM{*} (to denote all the hypotheses), or a comma-separated
-list of either hypothesis name, or {\tt (value of $H$)} or {\tt (type
-of $H$)}. Moreover, occurrences can be specified after every
-hypothesis after the {\TERM{at}} keyword. {\em concl} is either empty
-or \TERM{*}, and can be followed by occurences.
+the places where the abbreviation had to be folded (hypothese and/or
+conclusion). Clauses are the syntactic notion to denote in which parts
+of a goal a given transformation shold occur. Its basic notation is
+either \TERM{*} (meaning everywhere), or {\tt\textrm{\em hyps} |-
+\textrm{\em concl}} where {\em hyps} is either \TERM{*} (to denote all
+the hypotheses), or a comma-separated list of either hypothesis name,
+or {\tt (value of $H$)} or {\tt (type of $H$)}. Moreover, occurrences
+can be specified after every hypothesis after the {\TERM{at}}
+keyword. {\em concl} is either empty or \TERM{*}, and can be followed
+by occurences.
 
 \begin{transbox}
 \TRANS{in Goal}{in |- *}
@@ -433,6 +433,15 @@ or \TERM{*}, and can be followed by occurences.
 \subsection{Main changes in vernacular commands w.r.t. V7}
 
 
+\subsubsection{Require}
+
+The default behaviour of {\tt Require} is not to open the loaded
+module.
+
+\begin{transbox}
+\TRANS{Require Arith}{Require Import Arith}
+\end{transbox}
+
 \subsubsection{Binders}
 
 The binders of vernacular commands changed in the same way as those of
@@ -445,21 +454,15 @@ fixpoints. This also holds for parameters of inductive definitions.
       {Inductive and (A B:Prop): Prop := \\~~conj : A -> B -> and A B}
 \end{transbox}
 
-\subsubsection{Require}
-
-The default behaviour of {\tt Require} is not to open the loaded
-module.
+\subsubsection{Hints}
 
-\begin{transbox}
-\TRANS{Require Arith}{Require Import Arith}
-\end{transbox}
+Both {\tt Hints} and {\tt Hint} commands are beginning with {\tt Hint}.
 
-\subsubsection{Hints}
+Command {\tt HintDestruct} has disappeared.
 
-Names of hints are not supported anymore, except for {\tt HintDestruct}.
 
 The syntax of \emph{Extern} hints changed: the pattern and the tactic
-to be applied are separated by a \TERM{$\Rightarrow$}.
+to be applied are separated by a {\tt =>}.
 \begin{transbox}
 \TRANS{Hint name := Resolve (f ? x)}%
 {Hint Resolve (f _ x)}
@@ -469,14 +472,14 @@ to be applied are separated by a \TERM{$\Rightarrow$}.
 \TRANS{Hints Resolve f : db1 db2}{Hint Resolve f : db1 db2}
 \TRANS{Hints Immediate x y z}{Hint Immediate x y z}
 \TRANS{Hints Unfold x y z}{Hint Unfold x y z}
-\TRANS{\begin{tabular}{@{}l}
-  HintDestruct Local Conclusion \\
-  ~~name (f ? ?) 3 [Apply thm]
-  \end{tabular}}%
-{\begin{tabular}{@{}l}
- Hint Local Destuct name := \\
- ~~3 Conclusion (f _ _) => apply thm
- \end{tabular}}
+%% \TRANS{\begin{tabular}{@{}l}
+%%   HintDestruct Local Conclusion \\
+%%   ~~name (f ? ?) 3 [Apply thm]
+%%   \end{tabular}}%
+%% {\begin{tabular}{@{}l}
+%%  Hint Local Destuct name := \\
+%%  ~~3 Conclusion (f _ _) => apply thm
+%%  \end{tabular}}
 \end{transbox}
 
 
@@ -559,20 +562,20 @@ Type}, so several definitions in {\tt Type} are superseded by them.
 \section{A guide to translation}
 \label{Translation}
 
-\subsection{Overview of the translation process}
+%%\subsection{Overview of the translation process}
 
-Here is a short description of the tools of the translation package:
+Here is a short description of the tools involved in the translation process:
 \begin{description}
 \item{\tt coqc -translate}
 is the automatic translator. It is a parser/pretty-printer. This means
-that the translation is made by parsing using a parser of old syntax,
-and every command is printed using the new syntax. Many efforts were
-made to preserve as much as possible the quality of the presentation:
-it avoids expansion of syntax extensions, comments are not discarded
-and placed at the same place.
-\item{\tt tools/translate-v8} is a small shell-script that will help
-translate developments that compile with a Makefile with minimum
-requirements.
+that the translation is made by parsing every command using a parser
+of old syntax, which is printed using the new syntax. Many efforts
+were made to preserve as much as possible of the quality of the
+presentation: it avoids expansion of syntax extensions, comments are
+not discarded and placed at the same place.
+\item{\tt translate-v8} (in the translation package) is a small
+shell-script that will help translate developments that compile with a
+Makefile with minimum requirements.
 \end{description}
 
 \subsection{Preparation to translation}
@@ -580,7 +583,9 @@ requirements.
 This step is very important because most of work shall be done before
 translation. If a problem occurs during translation, it often means
 that you will have to modify the original source and restart the
-translation process.
+translation process. This also means that it is recommended not to
+edit the output of the translator since it would be overwritten if
+the translation has to be restarted.
 
 \subsubsection{Compilation with {\tt coqc -v7}}
 
@@ -607,7 +612,7 @@ try and make the translation.
 The preferred way is to use script {\tt translate-v8} if your development
 is compiled by a Makefile with the following constraints:
 \begin{itemize}
-\item compilation is achievd by invoke make without specifying a target
+\item compilation is achieved by invoking make without specifying a target
 \item options are passed to Coq with make variable COQFLAGS that
   includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML.
 \end{itemize}
@@ -675,10 +680,11 @@ x\_}
 \item avoid clash with new keywords by adding a trailing {\tt \_}
 \end{itemize}
 
-If the choices made by translation or in the following cases:
+If the choices made by translation is not satisfactory 
+or in the following cases:
 \begin{itemize}
-\item usage of latin letters
-\item usage if iso-latin characters in notations
+\item use of latin letters
+\item use of iso-latin characters in notations
 \end{itemize}
 the user should change his development prior to translation.
 
@@ -832,7 +838,7 @@ Notation "{ x }" := (my_embedding x) (at level 1)
   V8only (at level 0, x at level 99).
 \end{verbatim}
 
-\paragraph{Confilct: a notation conflicts with the V8 grammar}
+\paragraph{Conflict: a notation conflicts with the V8 grammar}
 
 Again, use the {\tt V8only} modifier to tell the translator to
 automatically take in charge the new syntax.
@@ -880,10 +886,10 @@ with left associativity). Even better, use interpretation scopes (look
 at the Reference Manual).
 
 
-\subsubsection{Strict implicits}
+\subsubsection{Strict implicit arguments}
 
 In the case you want to adopt the new semantics of {\tt Set Implicit
- Arguments} (only setting rigid arguments implicit), add the option
+ Arguments} (only setting rigid arguments as implicit), add the option
 {\tt -strict-implicit} to the translator.
 
 Warning: changing the number of implicit arguments can break the
diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex
index 0e43247cf6..7b30a82940 100755
--- a/doc/Tutorial.tex
+++ b/doc/Tutorial.tex
@@ -47,7 +47,7 @@ The standard invocation of \Coq\ delivers a message such as:
 \begin{flushleft}
 \begin{verbatim}
 unix:~> coqtop
-Welcome to Coq 8.0 (Dec 2003)
+Welcome to Coq 8.0 (Feb 2004)
 
 Coq < 
 \end{verbatim}
@@ -458,7 +458,7 @@ Actually, the tactic \verb+Split+ is just an abbreviation for \verb+apply conj.+
 What we have just seen is that the \verb:auto: tactic is more powerful than
 just a simple application of local hypotheses; it tries to apply as well 
 lemmas which have been specified as hints. A 
-\verb:Hints Resolve: command registers a
+\verb:Hint Resolve: command registers a
 lemma as a hint to be used from now on by the \verb:auto: tactic, whose power 
 may thus be incrementally augmented.
 
@@ -763,7 +763,7 @@ theorem in the first-order language declared in section
 \verb:R_sym_trans: has not been really significant, since we could have
 instead stated theorem \verb:refl_if: in its general form, and done 
 basically the same proof, obtaining \verb:R_symmetric: and
-\verb:R_transitive: as local hypotheses by initial \verb:Intros: rather
+\verb:R_transitive: as local hypotheses by initial \verb:intros: rather
 than as global hypotheses in the context. But if we had pursued the
 theory by proving more theorems about relation \verb:R:,
 we would have obtained all general statements at the closing of the section,
@@ -787,7 +787,8 @@ Lemma weird : (forall x:D, P x) ->  exists a, P a.
  intro UnivP.
 \end{coq_example}
 
-First of all, notice the pair of parentheses around \verb+(x:D)(P x)+ in
+First of all, notice the pair of parentheses around
+\verb+forall (x:D), P x+ in
 the statement of lemma \verb:weird:.
 If we had omitted them, \Coq's parser would have interpreted the
 statement as a truly trivial fact, since we would 
@@ -884,7 +885,7 @@ Finally, the excluded middle hypothesis is discharged only in
 Note that the name \verb:d: has vanished as well from
 the statements of \verb:weird: and \verb:drinker:, 
 since \Coq's pretty-printer replaces
-systematically a quantification such as \verb+(d:D)E+, where \verb:d:
+systematically a quantification such as \verb+forall d:D, E+, where \verb:d:
 does not occur in \verb:E:, by the functional notation \verb:D->E:. 
 Similarly the name \verb:EM: does not appear in \verb:drinker:. 
 
@@ -962,9 +963,9 @@ Qed.
 \end{coq_example}
 
 When one wants to rewrite an equality in a right to left fashion, we should
-use \verb:Rewrite <- E: rather than \verb:Rewrite E: or the equivalent
-\verb:Rewrite -> E:. 
-Let us now illustrate the tactic \verb:Replace:.
+use \verb:rewrite <- E: rather than \verb:rewrite E: or the equivalent
+\verb:rewrite -> E:. 
+Let us now illustrate the tactic \verb:replace:.
 \begin{coq_example}
 Hypothesis f10 : f 1 = f 0.
 Lemma L2 : f (f 1) = 0.
@@ -974,8 +975,8 @@ What happened here is that the replacement left the first subgoal to be
 proved, but another proof obligation was generated by the \verb:Replace:
 tactic, as the second subgoal. The first subgoal is solved immediately
 by applying lemma \verb:foo:; the second one transitivity and then 
-symmetry of equality, for instance with tactics \verb:Transitivity: and 
-\verb:Symmetry::
+symmetry of equality, for instance with tactics \verb:transitivity: and 
+\verb:symmetry::
 \begin{coq_example}
 apply foo.
 transitivity (f 0); symmetry; trivial.
@@ -1014,9 +1015,8 @@ combinator may be invoked by the tactic \verb:Exists: as above.
 Check ex_intro.
 \end{coq_example}
 
-Similarly, equality over Type is available, with notation 
-\verb:M==N:. The equality tactics process \verb:==: in the same way
-as \verb:=:.
+Equality over Type is available, with notation 
+\verb:M=N:.
 
 \section{Using definitions}
 
@@ -1054,9 +1054,10 @@ relation.
 Lemma subset_transitive : transitive set subset.
 \end{coq_example}
 
-In order to make any progress, one needs to use the definition of 
-\verb:transitive:. The \verb:unfold: tactic, which replaces all occurrences of a
-defined notion by its definition in the current goal, may be used here.
+In order to make any progress, one needs to use the definition of
+\verb:transitive:. The \verb:unfold: tactic, which replaces all
+occurrences of a defined notion by its definition in the current goal,
+may be used here.
 \begin{coq_example}
 unfold transitive.
 \end{coq_example}
@@ -1085,7 +1086,7 @@ intros.
 unfold subset in H.
 \end{coq_example}
 
-Finally, the tactic \verb:Red: does only unfolding of the head occurrence
+Finally, the tactic \verb:red: does only unfolding of the head occurrence
 of the current goal:
 \begin{coq_example}
 red.
@@ -1123,9 +1124,7 @@ mathematical constructions.
 Let us start with the collection of booleans, as they are specified
 in the \Coq's \verb:Prelude: module: 
 \begin{coq_example}
-Inductive bool :  Set :=
-  | true : bool
-  | false : bool.
+Inductive bool :  Set := true | false.
 \end{coq_example}
 
 Such a declaration defines several objects at once. First, a new
@@ -1221,8 +1220,8 @@ Definition addition (n m:nat) := prim_rec m (fun p rec:nat => S rec) n.
 \end{coq_example}
 
 That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
-according to its main constructor; when \verb:n=O:, we get \verb:m:;
- when \verb:n=(S p):, we get \verb:(S rec):, where \verb:rec: is the result
+according to its main constructor; when \verb:n = O:, we get \verb:m:;
+ when \verb:n = S p:, we get \verb:(S rec):, where \verb:rec: is the result
 of the recursive computation \verb+(addition p m)+. Let us verify it by
 asking \Coq~to compute for us say $2+3$:
 \begin{coq_example}
@@ -1230,7 +1229,7 @@ Eval compute in (addition (S (S O)) (S (S (S O)))).
 \end{coq_example}
 
 Actually, we do not have to do all explicitly. {\Coq} provides a
-special syntax {\tt Fixpoint/Cases} for generic primitive recursion,
+special syntax {\tt Fixpoint/match} for generic primitive recursion,
 and we could thus have defined directly addition as:
 
 \begin{coq_example}
@@ -1270,12 +1269,12 @@ What happened was that \verb:elim n:, in order to construct a \verb:Prop:
 (the initial goal) from a \verb:nat: (i.e. \verb:n:), appealed to the
 corresponding induction principle \verb:nat_ind: which we saw was indeed
 exactly Peano's induction scheme. Pattern-matching instantiated the 
-corresponding predicate \verb:P: to \verb+[n:nat]n=(plus n O)+, and we get
+corresponding predicate \verb:P: to \verb+fun n:nat => n = n + 0+, and we get
 as subgoals the corresponding instantiations of the base case \verb:(P O): ,
-and of the inductive step \verb+(y:nat)(P y)->(P (S y))+.
+and of the inductive step \verb+forall y:nat, P y -> P (S y)+.
 In each case we get an instance of function \verb:plus: in which its second
 argument starts with a constructor, and is thus amenable to simplification
-by primitive recursion. The \Coq~tactic \verb:Simpl: can be used for
+by primitive recursion. The \Coq~tactic \verb:simpl: can be used for
 this purpose:
 \begin{coq_example}
 simpl.
@@ -1368,8 +1367,8 @@ Lemma no_confusion : forall n:nat, 0 <> S n.
 \end{coq_example}
 
 First of all, we replace negation by its definition, by reducing the
-goal with tactic \verb:Red:; then we get contradiction by successive
-\verb:Intros::
+goal with tactic \verb:red:; then we get contradiction by successive
+\verb:intros::
 \begin{coq_example}
 red; intros n H.
 \end{coq_example}
@@ -1517,13 +1516,11 @@ of the libraries known by Coq, another module is also called
 all its contents, and all the contents of its subdirectories recursively are
 visible and accessible by a short (relative) name as \verb=Arith=.
 Notice also that modules or definitions not explicitly registered in
-a library are put in a default library called \verb=Scratch=.
+a library are put in a default library called \verb=Top=.
 
 The loading of a compiled file is quick, because the corresponding
 development is not type-checked again. 
 
-{\bf Warning}: \Coq~ does not yet provides parametric modules.
-
 \section{Creating your own modules}
 
 You may create your own modules, by writing \Coq~ commands in a file,
diff --git a/doc/macros.tex b/doc/macros.tex
index b16c4fb095..819a64d9b9 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -123,7 +123,7 @@
 \newcommand{\caseitems}{\nterm{match\_items}}
 \newcommand{\caseitem}{\nterm{match\_item}}
 \newcommand{\eqn}{\nterm{equation}}
-\newcommand{\ifitem}{\nterm{if\_item}}
+\newcommand{\ifitem}{\nterm{dep\_ret\_type}}
 \newcommand{\letclauses}{\nterm{letclauses}}
 \newcommand{\params}{\nterm{params}} % vernac
 \newcommand{\returntype}{\nterm{return\_type}}
@@ -364,15 +364,15 @@
 \newcommand{\CIPI}[1]{\CIP{#1}{I}{P}}
 \newcommand{\CIF}[1]{\mbox{$\{#1\}_{f_1.. f_n}$}}
 %BEGIN LATEX
-\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(\begin{array}[t]{l}#2:=#3
+\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(\begin{array}[t]{@{}l}#2:=#3
                                               \,)\end{array}$}}
-\newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](\begin{array}[t]{l}#3:=#4
+\newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](\begin{array}[t]{@{}l@{}}#3:=#4
                                                  \,)\end{array}$}}
 %END LATEX
 %HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}}
 %HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}}
 
-\newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{l}#3:=#4
+\newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4
                                                  \,)\end{array}$}}
 \newcommand{\Def}[4]{\mbox{{\sf Def}$(#1)(#2:=#3:#4)$}}
 \newcommand{\Assum}[3]{\mbox{{\sf Assum}$(#1)(#2:#3)$}}