*** empty log message ***

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

10 files changed, 691 insertions, 629 deletions

diff --git a/doc/Cases.tex b/doc/Cases.tex
index 39d06a414..aacdd0c80 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -8,12 +8,13 @@
 This section describes the full form of pattern-matching in {\Coq} terms.
 
 \asection{Patterns}\label{implementation} The full syntax of {\tt
-match} is presented in figure \ref{cases-grammar}.  Identifiers in
-patterns are either constructor names or variables. Any identifier
-that is not the constructor of an inductive or coinductive type is
-considered to be a variable. A variable name cannot occur more than
-once in a given pattern. It is recommended to start variable names by
-a lowercase letter.
+match} is presented in figures~\ref{term-syntax}
+and~\ref{term-syntax-aux}.  Identifiers in patterns are either
+constructor names or variables. Any identifier that is not the
+constructor of an inductive or coinductive type is considered to be a
+variable. A variable name cannot occur more than once in a given
+pattern. It is recommended to start variable names by a lowercase
+letter.
 
 If a pattern has the form $(c~\vec{x})$ where $c$ is a constructor
 symbol and $\vec{x}$ is a linear vector of variables, it is called
@@ -32,54 +33,6 @@ patterns separated with commas
 is also considered as a pattern and is called {\em multiple
 pattern}.
 
-Notice also that the annotation is mandatory when the sequence of equation is
-empty.
-
-\begin{figure}[t]
-\begin{rules}
-\DEFNT{match-expr}
-       \KWD{match}~\NT{case-items}~\OPT{\NT{case-type}}~\KWD{with}
-  ~\OPT{\TERMbar}~\OPT{\NT{branches}}~\KWD{end}        &&\RNAME{match}
-\SEPDEF
-\DEFNT{case-items}
-       \NT{case-item} ~\KWD{,} ~\NT{case-items}
-\nlsep \NT{case-item}
-\SEPDEF
-\DEFNT{case-item}
-       \NTL{constr}{100}~\OPTGR{\KWD{as}~\NT{name}}
-       ~\OPTGR{\KWD{in}~\NTL{constr}{100}}
-\SEPDEF
-\DEFNT{case-type}
-       \KWD{return}~\NTL{constr}{100}
-\SEPDEF
-\DEFNT{return-type}
-       \OPTGR{\KWD{as}~\NT{name}}~\NT{case-type}
-\SEPDEF
-\DEFNT{branches}
-       \NT{eqn}~\TERMbar~\NT{branches}
-\nlsep \NT{eqn}
-\SEPDEF
-\DEFNT{eqn}
-       \NT{pattern} ~\STARGR{\KWD{,}~\NT{pattern}}
-       ~\KWD{$\Rightarrow$}~\NT{constr}
-\SEPDEF
-\DEFNT{pattern}
-       \NT{reference}~\PLUS{\NT{pattern}}  & & \RNAME{constructor}
-\nlsep \NT{pattern}~\KWD{as}~\NT{ident}    & & \RNAME{alias}
-\nlsep \NT{pattern}~\KWD{\%}~\NT{ident}    & & \RNAME{scope-change}
-\nlsep \NT{reference}                      & & \RNAME{pattern-var}
-\nlsep \KWD{\_}                            & & \RNAME{hole}
-\nlsep \NT{int}                            &
-\nlsep \KWD{(}~\NT{tuple-pattern}~\KWD{)}
-\SEPDEF
-\DEFNT{tuple-pattern}
-       \NT{pattern}
-\nlsep \NT{tuple-pattern}~\KWD{,}~\NT{pattern} && \RNAME{pair}
-\end{rules}
-\caption{Extended match syntax}
-\label{cases-grammar}
-\end{figure}
-
 Since extended {\tt match} expressions are compiled into the primitive
 ones, the expressiveness of the theory remains the same. Once the
 stage of parsing has finished only simple patterns remain. An easy way
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 5bb620459..7f521f308 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -232,53 +232,14 @@ into a sequence of {\tt match} on simple patterns. Especially, a
 construction defined using the extended {\tt match} is printed under
 its expanded form.
 
-The syntax of the extended {\tt match} is presented in figure 
-\ref{ecases-grammar}.
-Remark that the annotation is mandatory when the set of equations is
-empty.
-
-\begin{figure}[t]
-\begin{tabular}{|rcl|}
-\hline
-%{\pattern}  & ::= & {\ident} \\
-% & $|$ & \_ \\
-% & $|$ & {\ident} \nelist{\pattern}{} \\
-% & $|$ & {\pattern} \texttt{as} {\ident} \\
-% & $|$ & {\pattern} \texttt{\%} {\ident} \\
-% & $|$ & \texttt{(} {\pattern} \texttt{)} \\
-% &&\\
-%
-{\eqn} & ++= &  \nelist{pattern}{,} \texttt{=>} {\term} \\
- && \\
-
-{\term} & ++= &  
-\texttt{match} \nelist{\caseitem}{,} \zeroone{{\tt return} {\type}}
-\texttt{with}\\
-&& \sequence{\eqn}{$|$}\\
-&&  \texttt{end} \\
-\hline
-\end{tabular}
-\caption{extended {\tt match} syntax.}
-\label{ecases-grammar}
-\end{figure}
-
 \SeeAlso chapter \ref{Mult-match-full}.
 
 \subsection{Pattern-matching on boolean values: the {\tt if} expression}
 \index{if@{\tt if ... then ... else}}
 
 For inductive types with exactly two constructors, it is possible to
-use a {\tt if ... then ... else} notation. This extends the syntax of
-terms as follows:
-
-\medskip
-\begin{tabular}{rcl}
-{\returntype} & ::= & \zeroone{{\tt as} {\ident}} {\tt return} {\type}\\
-{\term} & ++= & {\tt if} {\term} \zeroone{\returntype} {\tt then} {\term} {\tt else} {\term}\\
-\end{tabular}
-\medskip
-
-For instance, the definition
+use a {\tt if ... then ... else} notation. For instance, the
+definition
 
 \begin{coq_example}
 Definition not (b:bool) :=
@@ -301,18 +262,18 @@ Definition not (b:bool) := if b then false else true.
 \index{let in@{\tt let ... in}}
 \label{Letin}
 
-Terms in an inductive type having only one constructor, say {\tt foo}, have
-necessarily the form \texttt{(foo ...)}. In this case, the {\tt match}
-construction can be replaced by a {\tt let ... in ...} construction.
-This extends the syntax of terms as follows:
 
-\medskip
-\begin{tabular}{rcl}
-{\term} & ++= & {\tt let (} \nelist{\ident}{,} {\tt )} \zeroone{\returntype} {\tt :=}  {\term} {\tt in} {\term} \\
-\end{tabular}
-\medskip
 
-For instance, the definition
+Closed terms (that is not relying on any axiom or variable) in an
+inductive type having only one constructor, say {\tt foo}, have
+necessarily the form \texttt{(foo ...)}. In this case, the {\tt match}
+construction can be written with a syntax close to the {\tt let ... in
+...}  construction. Expression {\tt let
+(}~{\ident$_1$},\ldots,{\ident$_n$}~{\tt ) :=}~{\term$_0$}~{\tt
+in}~{\term$_1$} performs case analysis on {\term$_0$} which must be in
+an inductive type with one constructor with $n$ arguments. Variables
+{\ident$_1$}\ldots{\ident$_n$} are bound to the $n$ arguments of the
+constructor in expression {\term$_1$}. For instance, the definition
 
 \begin{coq_example}
 Definition fst (A B:Set) (H:A * B) := match H with
@@ -328,6 +289,9 @@ Reset fst.
 \begin{coq_example}
 Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x.
 \end{coq_example}
+Note however that reduction is slightly different from regular {\tt
+let ... in ...} construction since it can occur only if {\term$_0$}
+can be put in constructor form. Otherwise, reduction is blocked.
 
 The pretty-printing of a definition by matching on a
 irrefutable pattern can either be done using {\tt match} or the {\tt
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 13341bf99..7700bbfe6 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -336,16 +336,15 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\
  & $|$ & {\tt fix} {\fixpointbodies} &(\ref{fixpoints})\\
  & $|$ & {\tt cofix} {\cofixpointbodies} &(\ref{fixpoints})\\
- & $|$ &
-    {\tt let} {\ident} \sequence{\binderlet}{} {\typecstr} {\tt :=} {\term}
-    {\tt in} {\term} &(\ref{let-in})\\
+ & $|$ & {\tt let} {\idparams} {\tt :=} {\term}
+         {\tt in} {\term} &(\ref{let-in})\\
  & $|$ & {\tt let fix} {\fixpointbody} {\tt in} {\term} &(\ref{fixpoints})\\
  & $|$ & {\tt let cofix} {\cofixpointbody}
          {\tt in} {\term} &(\ref{fixpoints})\\
  & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt) :=} {\term}
-         {\tt in} {\term}  &(\ref{caseanalysis})\\
- & $|$ & {\tt if} {\term} \zeroone{\returntype} {\tt then} {\term}
-         {\tt else} {\term} &(\ref{caseanalysis})\\
+         {\tt in} {\term}  &(\ref{caseanalysis}, \ref{Mult-match})\\
+ & $|$ & {\tt if} {\ifitem} {\tt then} {\term}
+         {\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\
  & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\
  & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\
  & $|$ & {\term} \nelist{\termarg}{}&(\ref{applications})\\
@@ -353,13 +352,13 @@ chapter \ref{Addoc-syntax}.
             &(\ref{Implicits-explicitation})\\
  & $|$ & {\term} {\tt \%} {\ident} &(\ref{scopechange})\\
  & $|$ & {\tt match} \nelist{\caseitem}{\tt ,}
-                 \zeroone{\casetype} {\tt with} &\\
+                 \zeroone{\returntype} {\tt with} &\\
     &&   ~~~\zeroone{\zeroone{\tt |} \nelist{\eqn}{|}} {\tt end}
     &(\ref{caseanalysis})\\
  & $|$ & {\qualid} &(\ref{qualid})\\
  & $|$ & {\sort} &(\ref{Gallina-sorts})\\
  & $|$ & {\num} &(\ref{numerals})\\
- & $|$ & {\_} &(\ref{applications})\\
+ & $|$ & {\_} &(\ref{hole})\\
  & & &\\
 {\termarg} & ::= & {\term} &\\
  & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )}
@@ -367,22 +366,22 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )}
          &(\ref{Implicits-explicitation})\\
 &&&\\
-{\binderlist} & ::= & \nelist{\name}{} {\typecstr} &\\
+{\binderlist} & ::= & \nelist{\name}{} {\typecstr} & \ref{Binders} \\
  & $|$ & {\binder} \nelist{\binderlet}{} &\\
-{\binder} & ::= &   {\name} &\\
+&&&\\
+{\binder} & ::= &   {\name} & \ref{Binders} \\
  & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\  
-{\binderlet} & ::= & {\binder} &\\
+&&&\\
+{\binderlet} & ::= & {\binder} & \ref{Binders} \\
  & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
 & & &\\
 {\name} & \cn{}::= & {\ident} &\\
  & $|$ & {\tt \_} &\\
 &&&\\
-{\qualid} & ::= & {\ident} &\\
+{\qualid} & ::= & {\ident} & \\
  & $|$ & {\qualid} {\accessident} &\\
  & & &\\
-{\sort} & ::= & {\tt Prop} &\\
- & $|$ & {\tt Set} &\\
- & $|$ & {\tt Type} &\\
+{\sort} & ::= & {\tt Prop} ~$|$~ {\tt Set} ~$|$~ {\tt Type} &\\
 \hline
 \end{tabular}
 \caption{Syntax of terms}
@@ -398,6 +397,8 @@ chapter \ref{Addoc-syntax}.
 \begin{figure}[htb]
 \begin{tabular}{|lcl|}
 \hline
+{\idparams} & ::= &  {\ident} \sequence{\binderlet}{} {\typecstr} \\
+&&\\
 {\fixpointbodies} & ::= &
          {\fixpointbody} \\
  & $|$ & {\fixpointbody} {\tt with} \nelist{\fixpointbody}{{\tt with}}
@@ -410,19 +411,26 @@ chapter \ref{Addoc-syntax}.
 {\fixpointbody} & ::= &
     {\ident} \nelist{\binderlet}{} \zeroone{\annotation} {\typecstr}
     {\tt :=} {\term} \\
-{\cofixpointbody} & ::= &
-    {\ident} \sequence{\binderlet}{} {\typecstr} {\tt :=} {\term} \\
+{\cofixpointbody} & ::= & {\idparams} {\tt :=} {\term} \\
   & &\\
 {\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\ 
 &&\\
 {\caseitem} & ::= & {\term} \zeroone{{\tt as} \name}
      \zeroone{{\tt in} \term} \\
 &&\\
-{\casetype} & ::= & {\tt return} {\term} \\
+{\ifitem} & ::= & {\term} \zeroone{\zeroone{{\tt as} {\name}} {\returntype}} \\
 &&\\
-{\returntype} & ::= & \zeroone{{\tt as} {\name}} {\casetype} \\
+{\returntype} & ::= & {\tt return} {\term} \\
 &&\\
 {\eqn} & ::= & \nelist{\pattern}{\tt ,} {\tt =>} {\term}\\
+&&\\
+{\pattern} & ::= & {\qualid} \nelist{\pattern}{}  \\
+ & $|$ & {\pattern} {\tt as} {\ident}             \\
+ & $|$ & {\pattern} {\tt \%} {\ident}         \\
+ & $|$ & {\qualid}                              \\
+ & $|$ & {\tt \_}                                  \\
+ & $|$ & {\num}                                 \\
+ & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )}     \\
 \hline
 \end{tabular}
 \caption{Syntax of terms (continued)}
@@ -431,6 +439,15 @@ chapter \ref{Addoc-syntax}.
 \end{center}
 
 %%%%%%%
+
+\subsection{Types}
+
+{\Coq} terms are typed. {\Coq} types are recognized by the same
+syntactic class as {\term}. We denote by {\type} the semantic subclass
+of types inside the syntactic class {\term}.
+\index{type@{\type}}
+
+
 \subsection{Qualified identifiers and simple identifiers}
 \label{qualid}
 \label{ident}
@@ -481,12 +498,29 @@ subclass of the syntactic class {\term}.
 
 \noindent More on sorts can be found in section \ref{Sorts}.
 
-\subsection{Types}
-
-{\Coq} terms are typed. {\Coq} types are recognized by the same
-syntactic class as {\term}. We denote by {\type} the semantic subclass
-of types inside the syntactic class {\term}.
-\index{type@{\type}}
+\subsection{Binders}
+\label{Binders}
+\index{binders}
+
+Various constructions introduce variables which scope is some of its
+sub-expressions. There is a uniform syntax for this. A binder may be
+an (unqualified) identifier: the name to use to refer to this
+variable. If the variable is not to be used, its name can be {\tt
+\_}. When its type cannot be synthesized by the system, it can be
+specified with notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt
+)}. There is a notation for several variables sharing the same type:
+{\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt :}\,{\type}\,{\tt )}.
+
+Some constructions allow ``let-binders'', that is either a binder as
+defined above, or a variable with a value. The notation is {\tt
+(}\,{\ident}\,{\tt :=}\,{\term}\,{\tt )}. Only one variable can be
+introduced at the same time. It is also possible to give the type of
+the variable before the symbol {\tt :=}.
+
+The last kind of binders is the ``binder list''. It is either a list
+of let-binders (the first one not being a variable with value), or
+{\ident$_1$}\ldots{\ident$_n$}\,{\tt :}\,{\type} if all variables
+share the same type.
 
 \subsection{Abstractions}
 \label{abstractions}
@@ -494,24 +528,18 @@ of types inside the syntactic class {\term}.
 
 The expression ``{\tt fun} {\ident} {\tt :} \type {\tt =>} {\term}''
 denotes the {\em abstraction} of the variable {\ident} of type
-{\type}, over the term {\term}.
+{\type}, over the term {\term}. Put in another way, it is function of
+formal parameter {\ident} of type {\type} returning {\term}.
 
-One can abstract several variables successively: the notation {\tt
+Keyword {\tt fun} is followed by a ``binder list'', so any of the
+binders of section~\ref{Binders} apply. Internally, abstractions are
+only over one variable. Multiple variable binders are an iteration of
+the single variable abstraction: notation {\tt
 fun}~{\ident$_{1}$}~{\ldots}~{\ident$_{n}$}~{\tt :}~\type~{\tt
 =>}~{\term} stands for {\tt fun}~{\ident$_{1}$}~{\tt :}~\type~{\tt
-=>}~{\ldots}~{\tt fun}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}
-and the notation {\tt fun (}~{\localassums$_{1}$}~{\tt
-)}~{\ldots}~{\tt (}~{\localassums$_{m}$}~{\tt ) =>}~{\term} is a
-shorthand for {\tt fun}~{\localassums$_{1}$}~{\tt =>}~{\ldots}~{\tt
-fun}~{\localassums$_{m}$}~{\tt =>}~{\term}.
-
-\medskip
-\Rem The types of variables (and the {\tt :}) may be omitted in an
-abstraction when they can be synthesized by the system.
-
-\Rem Local definitions may appear inside parentheses. Obviously, this
-is expanded into a let-in.
-
+=>}~{\ldots}~{\tt fun}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}.
+Variables with a value expand to a local definition (see
+section~\ref{let-in}).
 
 \subsection{Products}
 \label{products}
@@ -519,17 +547,9 @@ is expanded into a let-in.
 
 The expression ``{\tt forall}~{\ident}~{\tt :}~\type~{\tt ,}~{\term}''
 denotes the {\em product} of the variable {\ident} of type {\type},
-over the term {\term}.
-
-Similarly, the expression {\tt forall} {\ident$_{1}$} {\ldots}
-{\ident$_{n}$} {\tt :} \type {\tt ,} {\term} is equivalent to {\tt
-forall} {\ident$_{1}$} {\tt :} \type {\tt ,} {\ldots} {\tt forall}
-{\ident$_{n}$} {\tt :} \type {\tt ,} {\term} and the expression {\tt
-forall (} {\typedidents$_{1}$} {\tt )} {\ldots} {\tt (}
-{\typedidents$_{m}$} {\tt ),} {\term} is a equivalent to {\tt
-forall}~{\typedidents$_{1}$} {\tt ,} {\ldots} {\tt forall}
-{\typedidents$_{m}$} {\tt ,} {\term}
-
+over the term {\term}. As for abstractions, {\tt forall} is followed
+by a binder list, and it is represented by an iteration of single
+variable products.
 
 Non dependent product types have a special notation ``$A$ {\tt ->}
 $B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. This is to stress
@@ -548,8 +568,27 @@ denotes the application of the term \term$_0$ to the arguments
 {\tt (} {\term$_0$} {\term$_1$} {\tt )} {\ldots} {\term$_n$} {\tt )}:
 associativity is to the left.
 
-%% explicit application
-%% \_
+When using implicit arguments mechanism, implicit positions can be
+forced a value with notation {\tt (}\,{\ident}\,{\tt
+:=}\,{\term}\,{\tt )} or {\tt (}\,{\num}\,{\tt
+:=}\,{\term}\,{\tt )}. See section~\ref{Implicits-explicitation} for
+details.
+
+\subsection{Type cast}
+\label{typecast}
+\index{Cast}
+
+The expression ``{\term}~{\tt :}~{\type}'' is a type cast
+expression. It forces checking that {\term} has type {\type}. It is
+identified to {\term}.
+
+\subsection{Inferable subterms}
+\label{hole}
+\index{\_}
+
+Since there are redundancies, a term can be type-checked without
+giving it in totality. Subterms that are left to guess by the
+type-checker are replaced by ``\_''.
 
 
 \subsection{Local definitions (let-in)}
@@ -558,47 +597,72 @@ associativity is to the left.
 \index{let-in}
 
 
-{\tt let}{\ident}{\tt :=}{\term$_1$}{\tt in}~{\term$_2$} denotes the local
-binding of \term$_1$ to the variable $\ident$ in \term$_2$.
+{\tt let}~{\ident}~{\tt :=}~{\term$_1$}~{\tt in}~{\term$_2$} denotes
+the local binding of \term$_1$ to the variable $\ident$ in
+\term$_2$. 
+
+There is a syntactic sugar for local definition of functions: {\tt
+let} {\ident} {\binder$_1$} \ldots {\binder$_n$} {\tt :=} {\term$_1$}
+{\tt in} {\term$_2$} stands for {\tt let} {\ident} {\tt := fun}
+{\binder$_1$} \ldots {\binder$_n$} {\tt in} {\term$_2$}.
 
 
 \subsection{Definition by case analysis}
 \label{caseanalysis}
 \index{match@{\tt match\ldots with\ldots end}}
 
-In a simple pattern \verb!(! \nelist{\ident}{} \verb!)!, the first {\ident}
-is intended to be a constructor.
 
-The expression {\tt match} {\term$_0$} {\tt with}
-{\pattern$_1$} {\tt =>} {\term$_1$} {\tt $|$} {\ldots} {\tt $|$}
-{\pattern$_n$} {\tt =>} {\term$_n$} {\tt end}, denotes a
-{\em pattern-matching} over the term {\term$_0$} (expected to be of an
-inductive type). 
+This paragraph only shows simple variants of case analysis. See
+section~\ref{Mult-match} and chapter~\ref{Mult-match-full} for
+explanations of the general form.
 
-The ... is the resulting type of the whole {\tt match}
-expression. Most of the time, when this type is the same as the
-types of all the {\term$_i$}, the annotation is not needed\footnote{except
-if no equation is given, to match the term in an empty type, e.g. the
-type \texttt{False}}. The annotation has to be given when the 
-resulting type of the whole {\tt match} depends on the actual {\term$_0$}
-matched.
+Objects of inductive types can be destructurated by a case-analysis
+construction, also called pattern-matching in functional languages. In
+its simple form, a case analysis expression is used to analyze the
+structure of an inductive objects (upon which constructor it is
+built).
 
-%% TODO: variants let (,,) and if/then/else
+The expression {\tt match} {\term$_0$} {\returntype} {\tt with}
+{\pattern$_1$} {\tt =>} {\term$_1$} {\tt $|$} {\ldots} {\tt $|$}
+{\pattern$_n$} {\tt =>} {\term$_n$} {\tt end}, denotes a {\em
+pattern-matching} over the term {\term$_0$} (expected to be of an
+inductive type $I$). {\term$_1$}\ldots{\term$_n$} are called branches. In
+a simple pattern \nelist{\ident}{}, the first {\ident} is intended to
+be a constructor. There should be a branch for every constructor of
+$I$.
+
+The {\returntype} is used to compute the resulting type of the whole
+{\tt match} expression and the type of the branches. Most of the time,
+when this type is the same as the types of all the {\term$_i$}, the
+annotation is not needed\footnote{except if no equation is given, to
+match the term in an empty type, e.g. the type \texttt{False}}. This
+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. \SeeAlso
+section~\ref{Mult-match} for details and examples.
 
 \subsection{Recursive functions}
 \label{fixpoints}
 \index{fix@{fix \ident$_i$\{\dots\}}}
 
-The expression ``{\tt fix} \ident$_1$ \binder$_1$ {\tt :} {\type$_1$}
+Expression ``{\tt fix} \ident$_1$ \binder$_1$ {\tt :} {\type$_1$}
 \texttt{:=} \term$_1$ {\tt with} {\ldots} {\tt with} \ident$_n$
 \binder$_n$~{\tt :} {\type$_n$} \texttt{:=} \term$_n$ {\tt for}
 {\ident$_i$}'' denotes the $i$th component of a block of functions
-defined by mutual well-founded recursion.
+defined by mutual well-founded recursion. It is the local counterpart
+of the {\tt Fixpoint} command. See section~\ref{Fixpoint} for more
+details. When $n=1$, the {\tt for}~{\ident$_i$} is omitted.
 
 The expression ``{\tt cofix} \ident$_1$~\binder$_1$ {\tt :}
-{\type$_1$} {\tt with} {\ldots} {\tt with} \ident$_n$ \binder$_n$
-{\tt :} {\type$_n$}~{\tt for} {\ident$_i$}'' denotes the $i$th
-component of a block of terms defined by a mutual guarded recursion.
+{\type$_1$} {\tt with} {\ldots} {\tt with} \ident$_n$ \binder$_n$ {\tt
+:} {\type$_n$}~{\tt for} {\ident$_i$}'' denotes the $i$th component of
+a block of terms defined by a mutual guarded co-recursion. It is the
+local counterpart of the {\tt CoFixpoint} command. See
+section~\ref{CoFixpoint} for more details. When $n=1$, the {\tt
+for}~{\ident$_i$} is omitted.
 
 The association of a single fixpoint and a local
 definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
@@ -607,22 +671,6 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
   applies for co-fixpoints.
 
 
-\subsection{Type cast}
-\label{typecast}
-\index{Cast}
-
-The expression ``{\term}~{\tt :}~{\type}'' is a type cast
-expression. It forces checking that {\term} has type {\type}. It is
-identified to {\term}.
-
-%% TODO
-
-\subsection{Scopes}
-\label{scopechange}
-\index{Scopes}
-
-%% TODO
-
 \section{The Vernacular}
 \label{Vernacular}
 
@@ -635,57 +683,49 @@ and ends with a dot.
 \begin{tabular}{|lcl|}
 \hline
 {\sentence} & ::= & {\declaration} \\
-           & $|$ & {\definition} \\
-           & $|$ & {\statement} \\
-           & $|$ & {\inductive} \\
-           & $|$ & {\fixpoint} \\
-           & $|$ & {\statement} ~~ {\proof} \\
-       & & \\
-{\params} & ::= & \nelist{\typedidents}{;} \\
-       & & \\
-{\declaration} & ::= & 
-  {\tt Axiom} {\ident} \verb.:. {\term} \verb:.: \\
- & $|$ &  {\declarationkeyword} {\params}  \verb:.: \\
-       & & \\
-{\declarationkeyword} & ::= & 
-{\tt Parameter} $|$ {\tt Parameters} \\
+            & $|$ & {\definition} \\
+            & $|$ & {\inductive} \\
+            & $|$ & {\fixpoint} \\
+            & $|$ & {\statement} \zeroone{\proof} \\
+&&\\
+%% Declarations
+{\declaration} & ::= & {\declarationkeyword} {\params} {\tt .} \\
+&&\\
+{\declarationkeyword} & ::= & {\tt Axiom} $|$ {\tt Conjecture} \\
+  & $|$  & {\tt Parameter} $|$  {\tt Parameters} \\
   & $|$  & {\tt Variable}  $|$ {\tt Variables}  \\
   & $|$  & {\tt Hypothesis}  $|$ {\tt Hypotheses}\\
-           & & \\
-
+&&\\
+{\params} & ::= & \nelist{\ident}{} {\tt :} {\term} \\
+          & $|$ & \nelist{\binder}{} \\
+&&\\
+%% Definitions
 {\definition} & ::= & 
-  {\tt Definition} {\ident} \zeroone{{\tt :} {\term}} \verb.:=. {\term} \verb:.: \\
- & $|$ &  {\tt Local} {\ident} \zeroone{{\tt :} {\term}} \verb.:=. {\term} \verb:.: \\
-           & & \\
-
+         {\tt Definition} {\idparams} {\tt :=} {\term} {\tt .} \\
+ & $|$ & {\tt Let} {\idparams} {\tt :=} {\term} {\tt .} \\
+&&\\
+%% Inductives
 {\inductive} & ::= & 
- {\tt Inductive} \nelist{\inductivebody}{with} 
-    \verb:.: \\
- & $|$ & 
- {\tt CoInductive} \nelist{\inductivebody}{with}
-    \verb:.: \\
+           {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\
+ & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\
            & & \\
 {\inductivebody} & ::= & 
-{\ident} \zeroone{{\tt [} {\params} {\tt ]}} \verb.:. {\term}
-      \verb.:=. 
-      \sequence{\constructor}{|} \\
-           & & \\
-{\constructor} & ::= & {\ident} \verb.:. {\term} \\
-  & &\\
-
-{\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} 
-   \verb:.: \\
-& $|$ &  {\tt CoFixpoint} \nelist{\cofixpointbody}{with} 
-   \verb:.: \\
-  & &\\
-
-{\statement} & ::= & {\tt Theorem} {\ident} {\tt :} {\term} \verb:.: \\
- & $|$ &  {\tt Lemma} {\ident} {\tt :} {\term} \verb:.: \\
- & $|$ &  {\tt Definition} {\ident} {\tt :} {\term} \verb:.: \\
-           & & \\
-
+  {\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt :=} \\
+   && ~~~\zeroone{\zeroone{\tt |} \nelist{\idparams}{|}} \\
+           & & \\  %% TODO: where ...
+%% Fixpoints
+{\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\
+       & $|$ &  {\tt CoFixpoint} \nelist{\cofixpointbody}{with} {\tt .} \\
+&&\\
+%% Lemmas & proofs
+{\statement} & ::= &
+  {\statkwd} {\ident} \sequence{\binderlet}{} {\tt :} {\term} {\tt .} \\
+&&\\
+  {\statkwd} & ::= & {\tt Theorem} $|$ {\tt Lemma} $|$ {\tt Definition} \\
+&&\\
 {\proof} & ::= & {\tt Proof} {\tt .} {\dots} {\tt Qed} {\tt .}\\
    & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Defined} {\tt .}\\
+   & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}\\
 \hline
 \end{tabular}
 \caption{Syntax of sentences}
@@ -693,66 +733,87 @@ and ends with a dot.
 The different kinds of command are described hereafter. They all suppose
 that the terms occurring in the sentences are well-typed.
 
+%%
+%% Axioms and Parameters
+%%
 \subsection{Declarations}\index{Declarations}\label{Declarations}
+
 The declaration mechanism allows the user to specify his own basic
 objects. Declared objects play the role of axioms or parameters in
 mathematics. A declared object is an {\ident} associated to a \term. A
-declaration is accepted by {\Coq} if and only if this {\term} is a correct type 
-in the current context of the declaration and \ident\ was
-not previously defined in the same module. This {\term}
-is considered to be the type, or specification, of the \ident.
+declaration is accepted by {\Coq} if and only if this {\term} is a
+correct type in the current context of the declaration and \ident\ was
+not previously defined in the same module. This {\term} is considered
+to be the type, or specification, of the \ident.
 
-\subsubsection{{\tt Axiom {\ident} : {\term}}.}
+\subsubsection{{\tt Axiom {\ident} :{\term} .}}
 \comindex{Axiom}
+\comindex{Parameter}\comindex{Parameters}
+\comindex{Conjecture}
 \label{Axiom}
-This command links {\term} to the name {\ident} as its specification in the
-global context. The fact asserted by {\term} is thus assumed
-as a postulate.
+
+This command links {\term} to the name {\ident} as its specification
+in the global context. The fact asserted by {\term} is thus assumed as
+a postulate.
 
 \begin{ErrMsgs}
 \item \errindex{Clash with previous constant {\ident}}
 \end{ErrMsgs}
 
 \begin{Variants} 
-\item {\tt Parameter {\ident} : {\term}.}
-  \comindex{Parameter}\\
+\item {\tt Parameter {\ident} :{\term}.} \\
   Is equivalent to {\tt Axiom {\ident} : {\term}}
-\item {\tt Parameter \nelist{\nelistwithoutblank{\ident}{,} : {\term}}{;} {\tt .}} \\
-%        Is equivalent to {\tt Axiom {\lident} : {\term}}  
-  Links the {\term}'s to the names comprising the lists \nelist{\nelist{\ident}{,} : {\term}}{;}.
-\item {\tt Conjecture {\ident} : {\term}.}
-  \comindex{Conjecture}\\
+
+\item {\tt Parameter {\ident$_1$}\ldots{\ident$_n$} {\tt :}{\term}.}\\
+  Adds $n$ parameters with specification {\term}
+
+\item
+ {\tt Parameter\,%
+(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
+\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
+{\term$_n$} {\tt )}.}\\ 
+  Adds $n$ blocks of parameters with different specifications.
+
+\item {\tt Conjecture {\ident} :{\term}.}\\
   Is equivalent to {\tt Axiom {\ident} : {\term}}.
 \end{Variants}
 
 \noindent {\bf Remark: } It is possible to replace {\tt Parameter} by
-{\tt Parameters} when more than one parameter are given.
+{\tt Parameters}.
 
-\subsubsection{{\tt Variable {\ident} : {\term}}.}\comindex{Variable}
+
+\subsubsection{{\tt Variable {\ident} :{\term}}.}
+\comindex{Variable}
 \comindex{Variables}
+\comindex{Hypothesis}
+\comindex{Hypotheses}
+
 This command links {\term} to the name {\ident} in the context of the
-current section (see \ref{Section} for a description of the section
-mechanism). The name {\ident} will be unknown when the current
-section will be closed. One says that the variable is {\em
-  discharged}. Using the {\tt Variable} command out of any section is
-equivalent to {\tt Axiom}.
+current section (see~\ref{Section} for a description of the section
+mechanism). When the current section is closed, name {\ident} will be
+unknown and every object using this variable will be explicitly
+parameterized (the variable is {\em discharged}). Using the {\tt
+Variable} command out of any section is equivalent to {\tt Axiom}.
 
 \begin{ErrMsgs}
 \item \errindex{Clash with previous constant {\ident}}
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Variable \nelist{\nelist{\ident}{,}:{\term}}{;} {\tt .}}\\
-  Links {\term} to the
-  names comprising the list \nelist{\nelist{\ident}{,}:{\term}}{;}
-\item {\tt Hypothesis \nelist{\nelist{\ident}{,} $\;$:$\;$ {\term}}{;} {\tt
- .}} \comindex{Hypothesis}\\  % Ligne trop longue
+\item {\tt Variable {\ident$_1$}\ldots{\ident$_n$} {\tt :}{\term}.}\\
+  Links {\term} to names {\ident$_1$}\ldots{\ident$_n$}.
+\item
+ {\tt Variable\,%
+(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
+\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
+{\term$_n$} {\tt )}.}\\ 
+  Adds $n$ blocks of variables with different specifications.
+\item {\tt Hypothesis {\ident} {\tt :}{\term}.} \\
   \texttt{Hypothesis} is a synonymous of \texttt{Variable}
 \end{Variants}
 
 \noindent {\bf Remark: } It is possible to replace {\tt Variable} by
-{\tt Variables} and \ml{Hypothesis} by {\tt Hypotheses}
- when more than one variable or one hypothesis are given.
+{\tt Variables} and \ml{Hypothesis} by {\tt Hypotheses}.
 
 It is advised to use the keywords \verb:Axiom: and \verb:Hypothesis:
 for logical postulates (i.e. when the assertion {\term} is of sort
@@ -760,17 +821,21 @@ for logical postulates (i.e. when the assertion {\term} is of sort
 \verb:Variable: in other cases (corresponding to the declaration of an
 abstract mathematical entity).
 
+%%
+%% Definitions
+%%
 \subsection{Definitions}\index{Definitions}\label{Simpl-definitions}
-Definitions differ from declarations since they allow to give a name
-to a term whereas declarations were just giving a type to a name. That
-is to say that the name of a defined object can be replaced at any
-time by its definition.  This replacement is called
-$\delta$-conversion\index{delta-reduction@$\delta$-reduction} (see section
-\ref{delta}).  A defined object is accepted by the system if and only if the
-defining term is well-typed in the current context of the definition.
-Then the type of the name is the type of term. The defined name is
-called a {\em constant}\index{Constant} and one says that {\it the
-  constant is added to the environment}\index{Environment}.
+Definitions differ from declarations in allowing to give a name to a
+term whereas declarations were just giving a type to a name. That is
+to say that the name of a defined object can be replaced at any time
+by its definition.  This replacement is called
+$\delta$-conversion\index{delta-reduction@$\delta$-reduction} (see
+section~\ref{delta}).  A defined object is accepted by the system if
+and only if the defining term is well-typed in the current context of
+the definition.  Then the type of the name is the type of term. The
+defined name is called a {\em constant}\index{Constant} and one says
+that {\it the constant is added to the
+environment}\index{Environment}.
 
 A formal presentation of constants and environments is given in
 section \ref{Typed-terms}.
@@ -786,10 +851,17 @@ environment, provided that {\term} is well-typed.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Definition {\ident} : {\term$_1$} := {\term$_2$}.} It
-  checks that the type of {\term$_2$} is definitionally equal to
+\item {\tt Definition {\ident} {\tt :}{\term$_1$} := {\term$_2$}.}\\
+  It checks that the type of {\term$_2$} is definitionally equal to
   {\term$_1$}, and registers {\ident} as being of type {\term$_1$},
   and bound to value {\term$_2$}.
+\item {\tt Definition {\ident} {\binder$_1$}\ldots{\binder$_n$}
+       {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
+  This is equivalent to \\
+   {\tt Definition\,{\ident}\,{\tt :\,forall}\,%
+       {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,%
+       {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
+       {\tt .}
 \end{Variants}
 
 \begin{ErrMsgs}
@@ -819,22 +891,9 @@ definition is a kind of {\em macro}.
 \SeeAlso \ref{Section} (section mechanism), \ref{Opaque},
 \ref{Transparent} (opaque/transparent constants), \ref{unfold}
 
-% Let comme forme de Definition n'existe plus
-%
-%\subsubsection{\tt Let {\ident} := {\term}.} 
-%\comindex{Let}
-
-%This command makes definition that are stronger than \texttt{Local},
-%and weaker than \texttt{Definition}. The name {\ident} will be known in the
-%current section and after having closed the current section, but will
-%be unknown after closing the section above the current section.
-
-%\begin{Variants}
-%\item {\tt Local {\ident} : {\term$_1$} := {\term$_2$}.}
-%\end{Variants}
-
-%\SeeAlso \ref{Section}
-
+%%
+%% Inductive Types
+%%
 \subsection{Inductive definitions}
 \index{Inductive definitions} \label{gal_Inductive_Definitions}
 \comindex{Inductive}\label{Inductive}
@@ -899,15 +958,29 @@ Check nat_ind.
 This is the well known structural induction principle over natural
 numbers, i.e. the second-order form of Peano's induction principle.
 It allows to prove some universal property of natural numbers ({\tt
-(n:nat)(P n)}) by induction on {\tt n}. Recall that {\tt (n:nat)(P n)}
-is \gallina's syntax for the universal quantification $\forall
-n:nat\cdot P(n).$\\ The types of {\tt nat\_rec} and {\tt nat\_rect}
-are similar, except that they pertain to {\tt (P:nat->Set)} and {\tt
-(P:nat->Type)} respectively . They correspond to primitive induction
-principles (allowing dependent types) respectively over sorts
-\verb:Set: and \verb:Type:. The constant {\ident}{\tt \_ind} is always
-provided, whereas {\ident}{\tt \_rec} and {\ident}{\tt \_rect} can be
-impossible to derive (for example, when {\ident} is a proposition).
+forall n:nat, P n}) by induction on {\tt n}.
+
+The types of {\tt nat\_rec} and {\tt nat\_rect} are similar, except
+that they pertain to {\tt (P:nat->Set)} and {\tt (P:nat->Type)}
+respectively . They correspond to primitive induction principles
+(allowing dependent types) respectively over sorts \verb:Set: and
+\verb:Type:. The constant {\ident}{\tt \_ind} is always provided,
+whereas {\ident}{\tt \_rec} and {\ident}{\tt \_rect} can be impossible
+to derive (for example, when {\ident} is a proposition).
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{Variants}
+\item 
+\begin{coq_example*}
+Inductive nat : Set := O | S (_:nat).
+\end{coq_example*}
+In the case where inductive types have no annotations (next section
+gives an example of such annotations), the positivity condition
+implies that a constructor can be defined by only giving the type of
+its arguments.
+\end{Variants}
 
 \subsubsection{Simple annotated inductive types}
 
@@ -947,44 +1020,55 @@ induction principle we got for {\tt nat}.
 \item \errindex{Type of Constructor not well-formed}
 \end{ErrMsgs}
 
-\begin{Variants}
-\item {\tt Inductive {\ident} [ {\params} ] : {\term} :=
-    {\ident$_1$}:{\term$_1$} | {\ldots} | {\ident$_n$}:\term$_n$.}\\ Allows
-  to define parameterized inductive types.\\
-  For instance, one can define
-  parameterized lists as:
+
+\subsubsection{Parameterized inductive types}
+
+Inductive types may be parameterized. Parameters differ from inductive
+type annotations in the fact that recursive invokations of inductive
+types must always be done with the same values of parameters as its
+specification.
+
+The general scheme is:
+\begin{center}
+{\tt Inductive} {\ident} {\binder$_1$}\ldots{\binder$_k$} : {\term} :=
+    {\ident$_1$}: {\term$_1$} | {\ldots} | {\ident$_n$}: \term$_n$
+{\tt .}
+\end{center}
+
+A typical example is the definition of polymorphic lists:
 \begin{coq_example*}
 Inductive list (X:Set) : Set :=
   | Nil : list X
   | Cons : X -> list X -> list X.
 \end{coq_example*}
-Notice that, in the type of {\tt Nil} and {\tt Cons}, we write {\tt
+
+Note that in the type of {\tt Nil} and {\tt Cons}, we write {\tt
   (list X)} and not just {\tt list}.\\ The constants {\tt Nil} and
 {\tt Cons} will have respectively types:
 
 \begin{coq_example}
 Check Nil.
-\end{coq_example}
-and
-
-\begin{coq_example}
 Check Cons.
 \end{coq_example}
 
 Types of destructors will be also quantified with {\tt (X:Set)}.
-\item  {\tt Inductive {\sort} {\ident} :=
-{\ident$_1$}:{\term$_1$} | {\ldots} | {\ident$_n$}:\term$_n$.}\\ 
-with {\sort} being one of {\tt Prop, Type, Set} is
-equivalent to \\ {\tt Inductive {\ident} : {\sort} :=
-  {\ident$_1$}:{\term$_1$} | {\ldots} | {\ident$_n$}:\term$_n$.}
-\item {\tt Inductive {\sort} {\ident} [ {\params} ]:=
-{\ident$_1$}:{\term$_1$} | {\ldots} | {\ident$_n$}:\term$_n$.}\\ 
-      Same as before but with parameters.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{Variants}
+\item
+\begin{coq_example*}
+Inductive list (X:Set) : Set := Nil | Cons (_:X) (_:list X).
+\end{coq_example*}
+This is an alternative definition of lists where we specify the
+arguments of the constructors rather than their full type.
 \end{Variants}
 
-\SeeAlso sections \ref{Cic-inductive-definitions}, \ref{elim}
+\SeeAlso sections \ref{Cic-inductive-definitions} and~\ref{elim}.
 
-\subsubsection{Mutually inductive types}
+
+\subsubsection{Mutually defined inductive types}
 \comindex{Mutual Inductive}\label{Mutual-Inductive}
 
 The definition of a block of mutually inductive types has the form:
@@ -1025,13 +1109,13 @@ inductive types The extended syntax is:
 
 \medskip
 {\tt 
-Inductive {{\ident$_1$} [{\rm\sl params} ] : {\type$_1$} :=  \\
+Inductive {{\ident$_1$} {\params} : {\type$_1$} :=  \\
 \mbox{}\hspace{0.4cm}  {\ident$_1^1$} : {\type$_1^1$} \\
 \mbox{}\hspace{0.1cm}| ..  \\
 \mbox{}\hspace{0.1cm}| {\ident$_{n_1}^1$} : {\type$_{n_1}^1$}  \\
 with\\
 \mbox{}\hspace{0.1cm} .. \\
-with {\ident$_m$} [{\rm\sl params} ] : {\type$_m$} := \\
+with {\ident$_m$} {\params} : {\type$_m$} := \\
 \mbox{}\hspace{0.4cm}{\ident$_1^m$} : {\type$_1^m$} \\
 \mbox{}\hspace{0.1cm}| .. \\
 \mbox{}\hspace{0.1cm}| {\ident$_{n_m}^m$} : {\type$_{n_m}^m$}.
@@ -1091,6 +1175,7 @@ definition.
 \SeeAlso \ref{Section}
 
 \subsubsection{Co-inductive types}
+\label{CoInductiveTypes}
 \comindex{CoInductive}
 
 The objects of an inductive type are well-founded with respect to the
@@ -1118,12 +1203,8 @@ analysis. For example, the usual destructors on streams
 \texttt{hd:Stream->nat} and \texttt{tl:Str->Str} can be defined as
 follows:
 \begin{coq_example}
-Definition hd (x:Stream) := match x with
-                            | Seq a s => a
-                            end.
-Definition tl (x:Stream) := match x with
-                            | Seq a s => s
-                            end.
+Definition hd (x:Stream) := let (a,s) := x in a.
+Definition tl (x:Stream) := let (a,s) := x in s.
 \end{coq_example}
 
 Definition of co-inductive predicates and blocks of mutually
@@ -1142,26 +1223,33 @@ $s_2$ we have to construct and infinite proof of equality, that is,
 an infinite object of type $(\texttt{EqSt}\;s_1\;s_2)$. We will see
 how to introduce infinite objects in section \ref{CoFixpoint}.
 
+%%
+%% (Co-)Fixpoints
+%%
 \subsection{Definition of recursive functions}
 
-\subsubsection{\tt Fixpoint {\ident} [ \ident$_1$ : \type$_1$ ] :
-\type$_0$ := \term$_0$}
+\subsubsection{\tt Fixpoint
+   {\ident} {\params} {\tt \{struct} \ident$_0$ {\tt \}} : type$_0$ :=
+   \term$_0$}
 \comindex{Fixpoint}\label{Fixpoint}
 
 This command allows to define inductive objects using a fixed point
-construction. The meaning of this declaration is to define {\it
-ident} a recursive function with one argument \ident$_1$ of type
-\term$_1$ such that ({\it ident}~\ident$_1$) has type \type$_0$ and is
+construction. The meaning of this declaration is to define {\it ident}
+a recursive function with arguments specified by
+{\binder$_1$}\ldots{\binder$_n$} such that {\it ident} applied to
+arguments corresponding to these binders has type \type$_0$, and is
 equivalent to the expression \term$_0$. The type of the {\ident} is
-consequently {(\ident$_1$ : \type$_1$)\type$_0$} and the value is
-equivalent to [\ident$_1$ : \type$_1$]\term$_0$.  The argument
-{\ident$_1$} (of type {\type$_1$}) is called the {\em recursive
-variable} of {\ident}.  Its type should be an inductive definition.
+consequently {\tt forall {\params} {\tt,} \type$_0$}
+and the value is equivalent to {\tt fun {\params} {\tt =>} \term$_0$}.
 
 To be accepted, a {\tt Fixpoint} definition has to satisfy some
-syntactical constraints on this recursive variable. They are needed to
-ensure that the {\tt Fixpoint} definition always terminates. For
-instance, one can define the addition function as :
+syntactical constraints on a special argument called the decreasing
+argument. They are needed to ensure that the {\tt Fixpoint} definition
+always terminates. The point of the {\tt \{struct \ident {\tt \}}}
+annotation is to let the user tell the system which argument decreases
+along the recursive calls. This annotation may be left implicit for
+fixpoints with one argument. For instance, one can define the addition
+function as :
 
 \begin{coq_example}
 Fixpoint add (n m:nat) {struct n} : nat :=
@@ -1184,21 +1272,6 @@ the inductive call {\tt (add p m)} the first argument actually
 decreases because it is a {\em pattern variable} coming from {\tt match
   n with}.
 
-\begin{Variants}
-\item {\tt Fixpoint {\ident} [ {\params} ] : \type$_0$ :=
-\term$_0$.}\\
-        It declares a list of identifiers with their type
-        usable in the type \type$_0$ and the definition body \term$_0$
-        and the last identifier in {\params} is the recursion variable.
-\item {\tt Fixpoint {\ident$_1$} [ {\params$_1$} ] :
-        {\type$_1$} := {\term$_1$}\\
-        with {\ldots} \\
-        with {\ident$_m$}  [ {\params$_m$} ] : {\type$_m$} := 
-        {\type$_m$}}\\
-        Allows to define simultaneously {\ident$_1$}, {\ldots},
-        {\ident$_m$}.
-\end{Variants}
-
 \Example The following definition is not correct and generates an
 error message:
 
@@ -1253,13 +1326,21 @@ Fixpoint mod2 (n:nat) : nat :=
 \end{coq_example*}
 In order to keep the strong normalisation property, the fixed point
 reduction will only be performed when the argument in position of the
-recursive variable (whose type should be in an inductive definition)
+decreasing argument (which type should be in an inductive definition)
 starts with a constructor.
 
 The {\tt Fixpoint} construction enjoys also the {\tt with} extension
 to define functions over mutually defined inductive types or more
 generally any mutually recursive definitions.
 
+\begin{Variants}
+\item {\tt Fixpoint {\ident$_1$} {\params$_1$} :{\type$_1$} := {\term$_1$}\\
+        with {\ldots} \\
+        with {\ident$_m$} {\params$_m$} :{\type$_m$} :=  {\type$_m$}}\\
+        Allows to define simultaneously {\ident$_1$}, {\ldots},
+        {\ident$_m$}.
+\end{Variants}
+
 \Example 
 The size of trees and forests can be defined the following way: 
 \begin{coq_eval}
@@ -1285,15 +1366,17 @@ Fixpoint tree_size (t:tree) : nat :=
 A generic command {\tt Scheme} is useful to build automatically various
 mutual induction principles. It is described in section \ref{Scheme}.
 
-\subsubsection{\tt CoFixpoint {\ident} :
-\type$_0$ := \term$_0$.}\comindex{CoFixpoint}\label{CoFixpoint}
+\subsubsection{\tt CoFixpoint {\ident} : \type$_0$ := \term$_0$.}
+\comindex{CoFixpoint}\label{CoFixpoint}
 
 The {\tt CoFixpoint} command introduces a method for constructing an
 infinite object of a coinduc\-tive type. For example, the stream
 containing all natural numbers can be introduced applying the
-following method to the number \texttt{O}:
-
-\begin{coq_example*}
+following method to the number \texttt{O} (see
+section~\ref{CoInductiveTypes} for the definition of {\tt Stream},
+{\tt hd} and {\tt tl}):
+\begin{coq_eval}
+Reset Initial.
 CoInductive Stream : Set :=
     Seq : nat -> Stream -> Stream.
 Definition hd (x:Stream) := match x with
@@ -1302,7 +1385,7 @@ Definition hd (x:Stream) := match x with
 Definition tl (x:Stream) := match x with
                             | Seq a s => s
                             end.
-\end{coq_example*}
+\end{coq_eval}
 \begin{coq_example}
 CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
 \end{coq_example}
@@ -1323,20 +1406,17 @@ Set Printing Depth 50.
 (********** The following is not correct and should produce **********)
 (***************** Error: Unguarded recursive call *******************)
 \end{coq_eval}
-\begin{coq_example*}
+\begin{coq_example}
 CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
   if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
-\end{coq_example*}
-
-\noindent Notice that the definition contains an unguarded recursive
-call of \texttt{filter} on the \texttt{else} branch of the test.
+\end{coq_example}
 
 The elimination of co-recursive definition is done lazily, i.e. the
 definition is expanded only when it occurs at the head of an
-application which is the argument of a case expression.  Isolate, it
-is considered as a canonical expression which is completely
-evaluated. We can test this using the command \texttt{Eval},
-which computes the normal forms of a term:
+application which is the argument of a case analysis expression.  In
+any other context, it is considered as a canonical expression which is
+completely evaluated. We can test this using the command
+\texttt{Eval}, which computes the normal forms of a term:
 
 \begin{coq_example}
 Eval compute in (from 0).
@@ -1344,15 +1424,21 @@ Eval compute in (hd (from 0)).
 Eval compute in (tl (from 0)).
 \end{coq_example}
 
-As in the \texttt{Fixpoint} command (cf. section~\ref{Fixpoint}), it
-is possible to introduce a block of mutually dependent methods. The
-general syntax for this case is:
-
-{\tt CoFixpoint {\ident$_1$}  :{\type$_1$} := {\term$_1$}\\
+\begin{Variants}
+\item{\tt CoFixpoint {\ident$_1$} {\params} :{\type$_1$} :=
+  {\term$_1$}}\\ As for most constructions, arguments of co-fixpoints
+  expressions can be introduced before the {\tt :=} sign.
+\item{\tt CoFixpoint {\ident$_1$} :{\type$_1$} := {\term$_1$}\\
      with\\
         \mbox{}\hspace{0.1cm} $\ldots$  \\
-        with {\ident$_m$}   : {\type$_m$} := {\term$_m$}}
+        with {\ident$_m$}   : {\type$_m$} := {\term$_m$}}\\
+As in the \texttt{Fixpoint} command (cf. section~\ref{Fixpoint}), it
+is possible to introduce a block of mutually dependent methods.
+\end{Variants}
 
+%%
+%% Theorems & Lemmas
+%%
 \subsection{Statement and proofs}
 
 A statement claims a goal of which the proof is then interactively done
@@ -1361,16 +1447,19 @@ found in chapter \ref{Proof-handling}.
 
 \subsubsection{\tt Theorem {\ident} : {\type}.}
 \comindex{Theorem}
+\comindex{Lemma}
+\comindex{Remark}
+\comindex{Fact}
+
 This command binds {\type} to the name {\ident} in the
 environment, provided that a proof of {\type} is next given.
 
 After a statement, Coq needs a proof.
 
 \begin{Variants} 
-
-\item {\tt Lemma {\ident} : {\type}.}\comindex{Lemma}\\ 
+\item {\tt Lemma {\ident} : {\type}.}\\ 
 It is a synonymous of \texttt{Theorem}
-\item {\tt Remark {\ident} : {\type}.}\comindex{Remark}\\ 
+\item {\tt Remark {\ident} : {\type}.}\\ 
 It is a synonymous of \texttt{Theorem}
 % Same as {\tt Theorem} except
 % that if this statement is in one or more levels of sections then the
@@ -1379,17 +1468,24 @@ It is a synonymous of \texttt{Theorem}
 % closed.
 % %All proofs of  persistent objects (such as theorems) referring to {\ident}
 % %within the section will be replaced by the proof of  {\ident}.
- \item {\tt Fact {\ident} : {\type}.}\comindex{Fact}\\ 
+ \item {\tt Fact {\ident} : {\type}.}\\ 
 It is a synonymous of \texttt{Theorem}
 % Same as {\tt Remark} except
 % that the innermost section name is dropped from the full name.
 \item {\tt Definition {\ident} : {\type}.} \\
 Allow to define a term of type {\type} using the proof editing mode. It
-behaves as {\tt Theorem} except the defined term will be transparent (see
-\ref{Transparent}, \ref{unfold}). 
+behaves as {\tt Theorem} but is intended for the interactive
+definition of expression which computational behaviour will be used by
+further commands. \SeeAlso~\ref{Transparent} and \ref{unfold}. 
 \end{Variants}
 
 \subsubsection{{\tt Proof} {\tt .} \dots {\tt Qed} {\tt .}}
+\comindex{Proof}
+\comindex{Qed}
+\comindex{Defined}
+\comindex{Save}
+\comindex{Goal}
+\comindex{Admitted}
 
 A proof starts by the keyword {\tt Proof}.  Then {\Coq} enters the
 proof editing mode until the proof is completed. The proof editing
@@ -1421,7 +1517,6 @@ To be able to unfold a proof, you should end the proof by {\tt Defined}
 
 \begin{Variants}
 \item {\tt Proof} {\tt .} \dots {\tt Defined} {\tt .}\\
-  \comindex{Proof}
   Same as {\tt Proof} {\tt .} \dots {\tt Qed} {\tt .} but the proof is
   then declared transparent (see \ref{Transparent}), which means it
   can be unfolded in conversion tactics (see \ref{Conversion-tactics}).
@@ -1431,12 +1526,10 @@ To be able to unfold a proof, you should end the proof by {\tt Defined}
   Same as {\tt Lemma} \ident {\tt :} \type \dots {\tt Save.}
   This is intended to be used in the interactive mode. Conversely to named
   lemmas, anonymous goals cannot be nested.
+\item {\tt Proof.} \dots {\tt Admitted.}\\
+  Turns the current conjecture into an axiom and exits editing of
+  current proof.
 \end{Variants}
-\comindex{Proof}
-\comindex{Qed}
-\comindex{Defined}
-\comindex{Save}
-\comindex{Goal}
 
 % Local Variables: 
 % mode: LaTeX
diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex
index 56a04954b..649cfc3a9 100755
--- a/doc/RefMan-int.tex
+++ b/doc/RefMan-int.tex
@@ -66,7 +66,7 @@ below.
   formalism. Chapter~\ref{Mod} describes the module system.
 
 \item The second part describes the proof engine. It is divided in
-  four chapters. Chapter~\ref{Vernacular-commands} presents all
+  five chapters. Chapter~\ref{Vernacular-commands} presents all
   commands (we call them \emph{vernacular commands}) that are not
   directly related to interactive proving: requests to the
   environment, complete or partial evaluation, loading and compiling
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index a8aefe781..c9173870d 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -53,23 +53,30 @@ with other precedence, which may be confusing.
 \hline
 Notation & Precedence & Associativity \\
 \hline
-\verb!<->! & 95 & no \\
-\verb!\/!  & 85 & right \\
-\verb!/\!  & 80 & right \\
-\verb!~!   & 75 & right \\
-\verb!=!   & 70 & no \\
-\verb!<>!  & 70 & no \\
-\verb!<!   & 70 & no \\
-\verb!>!   & 70 & no \\
-\verb!<=!  & 70 & no \\
-\verb!>=!  & 70 & no \\
-\verb!+!   & 50 & left \\
-\verb!-!   & 50 & left \\
-\verb!*!   & 40 & left \\
-\verb!/!   & 40 & left \\
-\verb!u-!  & 35 & right \\
-\verb!u/!  & 35 & right \\
-\verb!^!   & 30 & left \\
+\verb!_ <-> _! & 95 & no \\
+\verb!_ \/ _!  & 85 & right \\
+\verb!_ /\ _!  & 80 & right \\
+\verb!~ _!   & 75 & right \\
+\verb!_ = _!   & 70 & no \\
+\verb!_ = _ = _!   & 70 & no \\
+\verb!_ = _ :> _!   & 70 & no \\
+\verb!_ <> _!  & 70 & no \\
+\verb!_ <> _ :> _!  & 70 & no \\
+\verb!_ < _!   & 70 & no \\
+\verb!_ > _!   & 70 & no \\
+\verb!_ <= _!  & 70 & no \\
+\verb!_ >= _!  & 70 & no \\
+\verb!_ < _ < _! & 70 & no \\
+\verb!_ < _ <= _! & 70 & no \\
+\verb!_ <= _ < _! & 70 & no \\
+\verb!_ <= _ <= _! & 70 & no \\
+\verb!_ + _!   & 50 & left \\
+\verb!_ - _!   & 50 & left \\
+\verb!_ * _!   & 40 & left \\
+\verb!_ / _!   & 40 & left \\
+\verb!- _!  & 35 & right \\
+\verb!/ _!  & 35 & right \\
+\verb!_ ^ _!   & 30 & left \\
 \hline
 \end{tabular}
 \end{center}
@@ -83,9 +90,7 @@ The basic library of {\Coq} comes with the definitions of standard
 (intuitionistic) logical connectives (they are defined as inductive
 constructions). They are equipped with an appealing syntax enriching the
 (subclass {\form}) of the syntactic class {\term}. The syntax
-extension
-\footnote{This syntax is defined in module {\tt LogicSyntax}}
- is shown on figure \ref{formulas-syntax}.
+extension is shown on figure \ref{formulas-syntax}.
 
 \begin{figure}
 \label{formulas-syntax}
@@ -99,15 +104,14 @@ extension
   & $|$ & {\form} {\tt $\backslash$/} {\form} & ({\tt or})\\
   & $|$ & {\form} {\tt ->} {\form} & (\em{primitive implication})\\
   & $|$ & {\form} {\tt <->} {\form} & ({\tt iff})\\
-  & $|$ & {\tt (} {\ident} {\tt :} {\type} {\tt )}
+  & $|$ & {\tt forall} {\ident} {\tt :} {\type} {\tt ,}
   {\form} & (\em{primitive for all})\\
-  & $|$ & {\tt ( ALL} {\ident} \zeroone{{\tt :} {\specif}} {\tt |}
-  {\form} {\tt )} & ({\tt all})\\
-  & $|$ & {\tt ( EX} {\ident} \zeroone{{\tt :} {\specif}} {\tt
-  |} {\form} {\tt )}  & ({\tt ex})\\
-  & $|$ & {\tt ( EX} {\ident} \zeroone{{\tt :} {\specif}} {\tt
-  |} {\form}  {\tt \&} {\form} {\tt )} & ({\tt ex2})\\
+  & $|$ & {\tt exists} {\ident} \zeroone{{\tt :} {\specif}} {\tt
+  ,} {\form}  & ({\tt ex})\\
+  & $|$ & {\tt exists2} {\ident} \zeroone{{\tt :} {\specif}} {\tt
+  ,} {\form}  {\tt \&} {\form} & ({\tt ex2})\\
   & $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\
+  & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq})\\
 \hline
 \end{tabular}
 \end{center}
@@ -119,10 +123,7 @@ extension
 There is also a primitive universal quantification (it is a
 dependent product over a proposition). The primitive universal
 quantification allows both first-order and higher-order
-quantification. There is true reason to
-have the notation {\tt ( ALL} {\ident} \zeroone{{\tt :} {\specif}} {\tt
-|} {\form} {\tt )} propositions), except to have a notation dual of
-the notation for first-order existential quantification.
+quantification. 
 \caption{Syntax of formulas}
 \end{figure}
 
@@ -161,7 +162,7 @@ Abort All.
 \ttindex{or\_introl}
 \ttindex{or\_intror}
 \ttindex{iff}
-\ttindex{IF_then_else}
+\ttindex{IF\_then\_else}
 \begin{coq_example*}
 End Projections.
 Inductive or (A B:Prop) : Prop :=
@@ -319,17 +320,24 @@ again defined as inductive constructions over the sort
 \ttindex{option}
 \ttindex{Some}
 \ttindex{None}
+\ttindex{identity}
+\ttindex{refl\_identity}
 
 \begin{coq_example*}
 Inductive unit : Set := tt.
 Inductive bool : Set := true | false.
 Inductive nat : Set := O | S (n:nat).
 Inductive option (A:Set) : Set := Some (_:A) | None.
+Inductive identity (A:Type) (a:A) : A -> Type :=
+    refl_identity : identity A a a.
 \end{coq_example*}
 
 Note that zero is the letter \verb:O:, and {\sl not} the numeral
 \verb:0:.
 
+{\tt identity} is logically equivalent to equality but it lives in
+sort {\tt Set}. Computationaly, it behaves like {\tt unit}.
+
 We then define the disjoint sum of \verb:A+B: of two sets \verb:A: and
 \verb:B:, and their product \verb:A*B:.
 \ttindex{sum}
@@ -763,43 +771,23 @@ End Well_founded.
 \subsection{Accessing the {\Type} level}
 
 The basic library includes the definitions\footnote{This is in module
-{\tt Logic\_Type.v}} of logical quantifiers axiomatized at the
-\verb:Type: level. 
+{\tt Logic\_Type.v}} of the counterparts of some datatypes and logical
+quantifiers at the \verb:Type: level: negation, pair, and properties
+of {\tt identity}.
 
-\ttindex{all}
-\ttindex{inst}
-\ttindex{gen}
-\ttindex{EmptyT}
-\ttindex{UnitT}
 \ttindex{notT}
-
-\begin{coq_example*}
-Definition all (A:Type) (P:A->Prop) : Prop := forall x:A, P x.
-\end{coq_example*}
+\ttindex{prodT}
+\ttindex{pairT}
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example*}
-Section universal_quantification.
-Variable A :  Type.
-Variable P : A -> Prop.
-Theorem inst : forall x:A, (all (fun (x:A) => P x)) -> P x.
-Theorem gen : forall B:Prop, (forall y:A, B -> P y) -> B -> all P.
-\end{coq_example*}
-\begin{coq_eval}
-Abort All.
-\end{coq_eval}
-\begin{coq_example*}
-End universal_quantification.
+Definition notT (A:Type) := A -> False.
+Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B).
 \end{coq_example*}
 
-At the end, it defines datatypes at the {\Type} level.
 
-\begin{coq_example*}
-Definition notT (A:Type) := A -> False.
-Inductive identity (A:Type) (a:A) : A -> Type :=
-    refl_identity : identity A a a.
-\end{coq_example*}
+At the end, it defines datatypes at the {\Type} level.
 
 \section{The standard library}
 
@@ -845,55 +833,49 @@ through the \Coq\ homepage
 \index{Arithmetical notations}
 
 On figure \ref{zarith-syntax} is described the syntax of expressions
-for integer arithmetics. It is provided by requiring the module {\tt ZArith}.
+for integer arithmetics. It is provided by requiring and opening the
+module {\tt ZArith} and opening scope {\tt Z\_scope}.
 
 \ttindex{+}
 \ttindex{*}
 \ttindex{-}
+\ttindex{/}
+\ttindex{<=}
+\ttindex{>=}
+\ttindex{<}
+\ttindex{>}
+\ttindex{?=}
+\ttindex{mod}
+
+Figure~\ref{zarith-syntax} shows the notations provided by {\tt
+Z\_scope}. It specifies how notations are interpreted and, when not
+already reserved, the precedence and associativity.
 
-The {\tt +} and {\tt -} binary operators bind less than the {\tt *} operator
-which binds less than the {\tt |}~...~{\tt |} and {\tt -} unary
-operators which bind less than the others constructions.
-All the binary operators are left associative. The {\tt [}~...~{\tt ]}
-allows to escape the {\zarith} grammar.
-
-%% Should describe Z_scope instead
 \begin{figure}
 \begin{center}
-\begin{tabular}{|lcl|}
-\hline
-{\form} & ::= & {\tt `} {\zarithformula} {\tt `}\\
-  & & \\
-{\term} & ::= & {\tt `} {\zarith} {\tt `}\\
-  & & \\
-{\zarithformula} & ::= & {\zarith} {\tt =} {\zarith} \\
-   & $|$ & {\zarith} {\tt <=} {\zarith} \\
-   & $|$ & {\zarith} {\tt <} {\zarith} \\
-   & $|$ & {\zarith} {\tt >=} {\zarith} \\
-   & $|$ & {\zarith} {\tt >} {\zarith}  \\
-   & $|$ & {\zarith} {\tt =} {\zarith} {\tt =} {\zarith} \\
-   & $|$ & {\zarith} {\tt <=} {\zarith} {\tt <=} {\zarith} \\
-   & $|$ & {\zarith} {\tt <=} {\zarith} {\tt <} {\zarith} \\
-   & $|$ & {\zarith} {\tt <} {\zarith} {\tt <=} {\zarith} \\
-   & $|$ & {\zarith} {\tt <} {\zarith} {\tt <} {\zarith} \\
-   & $|$ & {\zarith} {\tt <>} {\zarith} \\
-   & $|$ & {\zarith} {\tt ?} {\tt =} {\zarith} \\
-  & & \\
-{\zarith}  & ::= & {\zarith} {\tt +} {\zarith} \\
-   & $|$ & {\zarith} {\tt -} {\zarith} \\
-   & $|$ & {\zarith} {\tt *} {\zarith} \\
-   & $|$ & {\tt |} {\zarith} {\tt |} \\
-   & $|$ & {\tt -} {\zarith} \\
-   & $|$ & {\ident} \\
-   & $|$ & {\tt [} {\term} {\tt ]} \\
-   & $|$ & {\tt (} \nelist{\zarith}{} {\tt )} \\
-   & $|$ & {\tt (} \nelist{\zarith}{,} {\tt )} \\
-   & $|$ & {\integer} \\
+\begin{tabular}{l|l|l|l}
+Notation & Interpretation & Precedence & Associativity\\
 \hline
+\verb!_ < _! & {\tt Zlt} \\
+\verb!x <= y! & {\tt Zle} \\
+\verb!_ > _! & {\tt Zgt} \\
+\verb!x >= y! & {\tt Zge} \\
+\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
+\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
+\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
+\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
+\verb!_ ?= _! & {\tt Zcompare} & 70 & no\\
+\verb!_ + _! & {\tt Zplus} \\
+\verb!_ - _! & {\tt Zminus} \\
+\verb!_ * _! & {\tt Zmult} \\
+\verb!_ / _! & {\tt Zdix} \\
+\verb!_ mod _! & {\tt Zmod} & 40 & no \\
+\verb!- _!  & {\tt Zopp} \\
+\verb!_ ^ _! & {\tt Zpower} \\
 \end{tabular}
 \end{center}
 \label{zarith-syntax}
-\caption{Syntax of expressions in integer arithmetics}
+\caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})}
 \end{figure}
 
 \subsection{Peano's arithmetic (\texttt{nat})}
@@ -910,9 +892,34 @@ defined here. This is provided by requiring the module {\tt Arith}.
 \subsubsection{Notations for real numbers}
 \index{Notations for real numbers}
 
-This is provided by requiring the module {\tt Reals}. This notation is
-very similar to the notation for integer arithmetics where Inverse
-(/x) and division (x/y) have been added.
+This is provided by requiring and opening the module {\tt Reals} and
+opening scope {\tt R\_scope}. This set of notations is very similar to
+the notation for integer arithmetics. The inverse function was added.
+\begin{figure}
+\begin{center}
+\begin{tabular}{l|l|l|l}
+Notation & Interpretation & Precedence & Associativity\\
+\hline
+\verb!_ < _! & {\tt Rlt} \\
+\verb!x <= y! & {\tt Rle} \\
+\verb!_ > _! & {\tt Rgt} \\
+\verb!x >= y! & {\tt Rge} \\
+\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
+\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
+\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
+\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
+\verb!_ + _! & {\tt Rplus} \\
+\verb!_ - _! & {\tt Rminus} \\
+\verb!_ * _! & {\tt Rmult} \\
+\verb!_ / _! & {\tt Rdix} \\
+\verb!- _!  & {\tt Ropp} \\
+\verb!/ _!  & {\tt Rinv} \\
+\verb!_ ^ _! & {\tt pow} \\
+\end{tabular}
+\end{center}
+\label{reals-syntax}
+\caption{Definition of the scope for real arithmetics ({\tt R\_scope})}
+\end{figure}
 
 \begin{coq_eval}
 Reset Initial.
@@ -987,10 +994,50 @@ Reset Initial.
 
 \subsection{List library}
 \index{Notations for lists}
+\ttindex{length}
+\ttindex{head}
+\ttindex{tail}
+\ttindex{app}
+\ttindex{rev}
+\ttindex{nth}
+\ttindex{map}
+\ttindex{flat\_map}
+\ttindex{fold\_left}
+\ttindex{fold\_right}
 
 Some elementary operations on polymorphic lists are defined here. They
 can be accessed by requiring module {\tt List}.
 
+It defines the following notions:
+\begin{center}
+\begin{tabular}{l|l}
+{\tt length} & length \\
+{\tt head} & first element (with default) \\
+{\tt tail} & all but first element \\
+{\tt app} & concatenation \\
+{\tt rev} & reverse \\
+{\tt nth} & accessing $n$-th element (with default) \\
+{\tt map} & applying a function \\
+{\tt flat\_map} & applying a function returning lists \\
+{\tt fold\_left} & iterator (from head to tail) \\
+{\tt fold\_right} & iterator (from tail to head) \\
+\end{tabular}
+\end{center}
+
+Table show notations available when opening scope {\tt list\_scope}.
+
+\begin{figure}
+\begin{center}
+\begin{tabular}{l|l|l|l}
+Notation & Interpretation & Precedence & Associativity\\
+\hline
+\verb!_ ++ _! & {\tt app} & 60 & right \\
+\verb!_ :: _! & {\tt cons} & 60 & right \\
+\end{tabular}
+\end{center}
+\label{list-syntax}
+\caption{Definition of the scope for lists ({\tt list\_scope})}
+\end{figure}
 
 
 \section{Users' contributions}
diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index b7be36257..a252a1fd9 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -72,7 +72,7 @@ is understood as
 \noindent{}\framebox[6in][l]
 {\parbox{6in}
 {\begin{center}
-\begin{tabular}{lp{0.1in}l}
+\begin{tabular}{lcl}
 {\tacexpr} & \cn{}::= &
            {\tacexpr} {\tt ;} {\tacexpr}\\
 & \cn{}| & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
@@ -135,30 +135,28 @@ is understood as
 \noindent{}\framebox[6in][l]
 {\parbox{6in}
 {\begin{center}
-\begin{tabular}{lp{0.1in}l}
-\tacarg & \cn{}::= & 
-           {\qualid}\\
-& \cn{}| & {\tt ()} \\
-& \cn{}| & {\tt ltac :} {\atom}\\
-& \cn{}| & {\term}\\
+\begin{tabular}{lcl}
+\tacarg & ::= & 
+        {\qualid}\\
+& $|$ & {\tt ()} \\
+& $|$ & {\tt ltac :} {\atom}\\
+& $|$ & {\term}\\
 \\
-\letclause & \cn{}::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\
+\letclause & ::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\
 \\
-\recclause & \cn{}::= & {\ident} \nelist{\name}{} {\tt :=} {\tacexpr}\\
+\recclause & ::= & {\ident} \nelist{\name}{} {\tt :=} {\tacexpr}\\
 \\
-\contextrule & \cn{}::= &
-  \nelist{\contexthyps}{\tt ,} {\tt |-}
-{\cpattern} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt \_ =>} {\tacexpr}\\
+\contextrule & ::= &
+  \nelist{\contexthyps}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\
+& $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
+& $|$ & {\tt \_ =>} {\tacexpr}\\
 \\
-\contexthyps & \cn{}::= &
-           {\name} {\tt :} {\cpattern}\\
+\contexthyps & ::= & {\name} {\tt :} {\cpattern}\\
 \\
-\matchrule & \cn{}::= &
+\matchrule & ::= &
            {\cpattern} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt \_ =>} {\tacexpr}\\
+& $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\
+& $|$ & {\tt \_ =>} {\tacexpr}\\
 \end{tabular}
 \end{center}}}
 \caption{Syntax of the tactic language (continued)}
@@ -169,10 +167,10 @@ is understood as
 \noindent{}\framebox[6in][l]
 {\parbox{6in}
 {\begin{center}
-\begin{tabular}{lp{0.1in}l}
-\nterm{top} & \cn{}::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
+\begin{tabular}{lcl}
+\nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
 \\
-\nterm{ltac\_def} & \cn{}::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr}
+\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr}
 \end{tabular}
 \end{center}}}
 \caption{Tactic toplevel definitions}
@@ -247,10 +245,10 @@ of Ltac.
 \index{;@{\tt ;}}
 \index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}
 
-A sequence is an expression of the following form:\\
-
-{\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$\\
-
+A sequence is an expression of the following form:
+\begin{center}
+{\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
+\end{center}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
 $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied
 and $v_2$ is applied to every subgoal generated by the application of
@@ -261,11 +259,11 @@ $v_1$. Sequence is left associating.
 \index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
 \index{Tacticals!; [ | ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
 
-We can generalize the previous sequence operator by:\\
-
+We can generalize the previous sequence operator by:
+\begin{center}
 {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
-{\tacexpr}$_n$ {\tt ]}\\
-
+{\tacexpr}$_n$ {\tt ]}
+\end{center}
 {\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is
 applied and $v_i$ is applied to the $i$-th generated subgoal by the
 application of $v_0$, for $=1,...,n$. It fails if the application of
@@ -275,10 +273,10 @@ $v_0$ does not generate exactly $n$ subgoals.
 \tacindex{do}
 \index{Tacticals!do@{\tt do}}
 
-There is a for loop that repeats a tactic {\num} times:\\
-
-{\tt do} {\num} {\tacexpr}\\
-
+There is a for loop that repeats a tactic {\num} times:
+\begin{center}
+{\tt do} {\num} {\tacexpr}
+\end{center}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied {\num} times. Supposing ${\num}>1$, after the first
 application of $v$, $v$ is applied, at least once, to the generated
@@ -289,10 +287,10 @@ the {\num} applications have been completed.
 \tacindex{repeat}
 \index{Tacticals!repeat@{\tt repeat}}
 
-We have a repeat loop with:\\
-
-{\tt repeat} {\tacexpr}\\
-
+We have a repeat loop with:
+\begin{center}
+{\tt repeat} {\tacexpr}
+\end{center}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied until it fails. Supposing $n>1$, after the first application
 of $v$, $v$ is applied, at least once, to the generated subgoals and
@@ -303,10 +301,10 @@ fails.
 \tacindex{try}
 \index{Tacticals!try@{\tt try}}
 
-We can catch the tactic errors with:\\
-
-{\tt try} {\tacexpr}\\
-
+We can catch the tactic errors with:
+\begin{center}
+{\tt try} {\tacexpr}
+\end{center}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied. If the application of $v$ fails, it catches the error and
 leaves the goal unchanged. If the level of the exception is positive,
@@ -315,10 +313,10 @@ then the exception is re-raised with its level decremented.
 \subsubsection{Detecting progress}
 \tacindex{progress}
 
-We can check if a tactic made progress with:\\
-
-{\tt progress} {\tacexpr}\\
-
+We can check if a tactic made progress with:
+\begin{center}
+{\tt progress} {\tacexpr}
+\end{center}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
 applied. If the application of $v$ produced one subgoal equal to the
 initial goal (up to syntactical equality), then an error of level 0 is
@@ -331,10 +329,10 @@ raised.
 \tacindex{||}
 \index{Tacticals!orelse@{\tt ||}}
 
-We can easily branch with the following structure:\\
-
-{\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$\\
-
+We can easily branch with the following structure:
+\begin{center}
+{\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$
+\end{center}
 {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
 $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if
 it fails then $v_2$ is applied. Branching is left associating.
@@ -344,13 +342,13 @@ it fails then $v_2$ is applied. Branching is left associating.
 \index{Tacticals!first@{\tt first}}
 
 We may consider the first tactic to work (i.e. which does not fail) among a
-panel of tactics:\\
-
-{\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\
-
+panel of tactics:
+\begin{center}
+{\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+\end{center}
 {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
 $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it works, it stops else it
-tries to apply $v_2$ and so on. It fails when there is no applicable tactic.\\
+tries to apply $v_2$ and so on. It fails when there is no applicable tactic.
 
 \ErrMsg \errindex{No applicable tactic}
 
@@ -359,13 +357,13 @@ tries to apply $v_2$ and so on. It fails when there is no applicable tactic.\\
 \index{Tacticals!solve@{\tt solve}}
 
 We may consider the first to solve (i.e. which generates no subgoal) among a
-panel of tactics:\\
-
-{\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\
-
+panel of tactics:
+\begin{center}
+{\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+\end{center}
 {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for 
 $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it solves, it stops else it
-tries to apply $v_2$ and so on. It fails if there is no solving tactic.\\
+tries to apply $v_2$ and so on. It fails if there is no solving tactic.
 
 \ErrMsg \errindex{Cannot solve the goal}
 
@@ -374,10 +372,10 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic.\\
 \index{Tacticals!idtac@{\tt idtac}}
 
 The constant {\tt idtac} is the identity tactic: it leaves any goal
-unchanged but it appears in the proof script.\\
-
-{\tt idtac} and {\tt idtac "message"}\\
-
+unchanged but it appears in the proof script.
+\begin{center}
+{\tt idtac} and {\tt idtac "message"}
+\end{center}
 The latter variant prints the string on the standard output.
 
 \subsubsection{Failing}
@@ -386,10 +384,10 @@ The latter variant prints the string on the standard output.
 
 The tactic {\tt fail} is the always-failing tactic: it does not solve
 any goal. It is useful for defining other tacticals since it can be
-catched by {\tt try} or {\tt match goal}. There are three variants:\\
-
-{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}  \\
-
+catched by {\tt try} or {\tt match goal}. There are three variants:
+\begin{center}
+{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}
+\end{center}
 The number $n$ is the failure level. If no level is specified, it
 defaults to $0$.  The level is used by {\tt try} and {\tt match goal}.
 If $0$, it makes {\tt match goal} considering the next clause
@@ -428,10 +426,10 @@ argument is required.
 
 \subsubsection{Application}
 
-An application is an expression of the following form:\\
-
-{\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$\\
-
+An application is an expression of the following form:
+\begin{center}
+{\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$
+\end{center}
 The reference {\qualid} must be bound to some defined tactic
 definition expecting at least $n$ arguments.  The expressions
 {\tacexpr}$_i$ are evaluated to $v_i$, for $i=1,...,n$.
@@ -446,10 +444,10 @@ definition expecting at least $n$ arguments.  The expressions
 \tacindex{fun}
 
 A parameterized tactic can be built anonymously (without resorting to
-local definitions) with:\\
-
-{\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr}\\
-
+local definitions) with:
+\begin{center}
+{\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr}
+\end{center}
 Indeed, local definitions of functions are a syntactic sugar for
 binding a {\tt fun} tactic to an identifier.
 
@@ -477,21 +475,21 @@ pattern {\_} matches any term and shunts all remaining patterns if
 any. If {\tacexpr}$_1$ evaluates to a tactic, this tactic is not
 immediately applied to the current goal (in contrast with {\tt match
 goal}). If all clauses fail (in particular, there is no pattern {\_})
-then a no-matching error is raised. \\
+then a no-matching error is raised.
 
 \begin{ErrMsgs}
 \item \errindex{No matching clauses for match}\\
-\hx{4}No pattern can be used and, in particular, there is no {\tt \_} pattern.
+No pattern can be used and, in particular, there is no {\tt \_} pattern.
 \item \errindex{Argument of match does not evaluate to a term}\\
-\hx{4}This happens when {\tacexpr} does not denote a term.
+This happens when {\tacexpr} does not denote a term.
 \end{ErrMsgs}
 
 \tacindex{context (in pattern)}
 There is a special form of patterns to match a subterm against the
-pattern:\\
-
-{\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}\\
-
+pattern:
+\begin{center}
+{\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}
+\end{center}
 It matches any term which one subterm matches {\cpattern}. If there is
 a match, the optional {\ident} is assign the ``matched context'', that
 is the initial term where the matched subterm is replaced by a
@@ -537,11 +535,13 @@ hypotheses is tried with the same proof context pattern. If there is
 no other combination of hypotheses then the second proof context
 pattern is tried and so on. If the next to last proof context pattern
 fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$
-is applied.\\
+is applied.
+
+\ErrMsg \errindex{No matching clauses for match goal}
 
-\ErrMsg \errindex{No matching clauses for match goal}\\
-\hx{4}No goal pattern can be used and, in particular, there is no {\tt
+No goal pattern can be used and, in particular, there is no {\tt
 \_} goal pattern.
+\medskip
 
 It is important to know that each hypothesis of the goal can be
 matched by at most one hypothesis pattern. The order of matching is
@@ -557,9 +557,9 @@ the {\tt match reverse goal with} variant.
 The following expression is not a tactic in the sense that it does not
 produce subgoals but generates a term to be used in tactic
 expressions:
-
+\begin{center}
 {\tt context} {\ident} {\tt [} {\tacexpr} {\tt ]}
-
+\end{center}
 {\ident} must denote a context variable bound by a {\tt context}
 pattern of a {\tt match} expression. This expression evaluates
 replaces the hole of the value of {\ident} by the value of
@@ -575,18 +575,16 @@ the system decide a name with the {\tt intro} tactic is not so good
 since it is very awkward to retrieve the name the system gave.
 
 As before, the following expression returns a term:
-
+\begin{center}
 {\tt fresh} {\qstring}
-
+\end{center}
 It evaluates to an identifier unbound in the goal, which is obtained
 by padding {\qstring} with a number if necessary. If no name is given,
 the prefix is {\tt H}.
 
-\subsubsection{Type of a constr}
+\subsubsection{{\tt type of} {\term}}
 \tacindex{type of}
 
-{\tt type of} {\term}
-
 This tactic computes the type of {\term}.
 
 
@@ -594,9 +592,9 @@ This tactic computes the type of {\term}.
 \tacindex{eval}
 
 Evaluation of a term can be performed with:
-
-{\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
-
+\begin{center}
+{\tt eval} {\nterm{redexpr}} {\tt in} {\term}
+\end{center}
 where \nterm{redexpr} is a reduction tactic among {\tt red}, {\tt
 hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold},
 {\tt fold}, {\tt pattern}.
@@ -635,30 +633,28 @@ without having to cut manually the proof in smaller lemmas.
 \subsection{Tactic toplevel definitions}
 \comindex{Ltac}
 
-Basically, tactics toplevel definitions are made as follows:\\
-
+Basically, tactics toplevel definitions are made as follows:
 %{\tt Tactic Definition} {\ident} {\tt :=} {\tacexpr}\\
 %
 %{\tacexpr} is evaluated to $v$ and $v$ is associated to {\ident}. Next, every
 %script is evaluated by substituting $v$ to {\ident}.
 %
 %We can define functional definitions by:\\
-
+\begin{center}
 {\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=}
-{\tacexpr}\\
-
-\noindent This defines a new tactic that can be used in any tactic
-script or new tactic toplevel definition.
-
-\Rem The preceding definition can equivalently be written:\\
+{\tacexpr}
+\end{center}
+This defines a new tactic that can be used in any tactic script or new
+tactic toplevel definition.
 
+\Rem The preceding definition can equivalently be written:
+\begin{center}
 {\tt Ltac} {\ident} {\tt := fun} {\ident}$_1$ ... {\ident}$_n$
-{\tt =>} {\tacexpr}\\
-
-\noindent Recursive and mutual recursive function definitions are also
+{\tt =>} {\tacexpr}
+\end{center}
+Recursive and mutual recursive function definitions are also
 possible with the syntax:
-\medskip
-
+\begin{center}
 \begin{tabular}{l}
 {\tt Ltac} {\ident}$_1$ {\ident}$_{1,1}$ ...
 {\ident}$_{1,m_1}$~~{\tt :=} {\tacexpr}$_1$\\
@@ -668,6 +664,7 @@ possible with the syntax:
 {\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=}
 {\tacexpr}$_n$
 \end{tabular}
+\end{center}
 
 %This definition bloc is a set of definitions (use of
 %the same previous syntactical sugar) and the other scripts are evaluated as
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index d5604ecc4..9439d202f 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -401,6 +401,8 @@ Locate "'exists' _ , _".
 \subsection{Notations in scope}
 
 \subsection{Activation of interpretation scopes}
+\label{scopechange}
+\index{\%}
 
 % Open (Local) Scope
 % Close (Local) Scope
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 9361d3f05..3d09c1249 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -2448,7 +2448,8 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is:
 \noindent where {\sl hint\_definition} is one of the following expressions:
 
 \begin{itemize}
-\item \texttt{Resolve} {\term} \index[command]{Hint!Resolve}\\
+\item \texttt{Resolve} {\term} \index[command]{Hint!Resolve}
+
   This command adds {\tt apply {\term}} to the hint list
   with the head symbol of the type of \term. The cost of that hint is
   the number of subgoals generated by {\tt apply {\term}}.
@@ -2466,17 +2467,20 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is:
   only by \texttt{eauto} is a transitivity lemma.
 
   \begin{ErrMsgs}
-  \item \errindex{Bound head variable} \\
+  \item \errindex{Bound head variable}
+
     The head symbol of the type of {\term} is a bound variable such
     that this tactic cannot be associated to a constant.
-  \item \term\ \errindex{cannot be used as a hint} \\
+  \item \term\ \errindex{cannot be used as a hint}
+
     The type of \term\ contains products over variables which do not
     appear in the conclusion. A typical example is a transitivity axiom.
     In that case the {\tt apply} tactic fails, and thus is useless.
   \end{ErrMsgs}
 
   \begin{Variants}
-    \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$} \\
+    \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$}
+
       Adds each \texttt{Resolve} {\term$_i$}.
   \end{Variants}
 
@@ -2497,12 +2501,13 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is:
   so that it is not used by {\tt trivial} itself.
 
   \begin{ErrMsgs}
-  \item \errindex{Bound head variable}\\
-  \item \term\ \errindex{cannot be used as a hint} \\
+  \item \errindex{Bound head variable}
+  \item \term\ \errindex{cannot be used as a hint}
   \end{ErrMsgs}
 
   \begin{Variants}
-    \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$} \\
+    \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$}
+
       Adds each \texttt{Immediate} {\term$_i$}.
   \end{Variants}
 
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index eb5f87318..7a411e822 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -9,12 +9,12 @@ illustrate their behavior.
 \label{refine-example}
 
 This tactic applies to any goal. It behaves like {\tt exact} with a
-big difference : the user can leave some holes (denoted by \texttt{?} or 
-{\tt (?::}{\it type}{\tt )}) in the term. 
+big difference : the user can leave some holes (denoted by \texttt{\_} or 
+{\tt (\_:}{\it type}{\tt )}) in the term. 
 {\tt refine} will generate as many
 subgoals as they are holes in the term. The type of holes must be
 either synthesized by the system or declared by an
-explicit cast like \verb|(?::nat->Prop)|. This low-level
+explicit cast like \verb|(\_:nat->Prop)|. This low-level
 tactic can be useful to advanced users.
 
 %\firstexample
@@ -145,7 +145,7 @@ apply (Rtrans n m p).
 Undo.
 \end{coq_eval}
 
-More elegantly, {\tt apply Rtrans with y:=m} allows to only mention
+More elegantly, {\tt apply Rtrans with (y:=m)} allows to only mention
 the unknown {\tt m}:
 
 \begin{coq_example}
@@ -185,8 +185,7 @@ of finding {\tt m}. Then one can apply the hypotheses {\tt Rnm} and {\tt
 Rmp}. This instantiates the existential variable and completes the proof.
 
 \begin{coq_example}
-
-  eapply Rtrans.
+eapply Rtrans.
 apply Rnm.
 apply Rmp.
 \end{coq_example}
@@ -218,8 +217,7 @@ with forest : Set :=
   | leaf : B -> forest
   | cons : tree -> forest -> forest.
 
-Scheme tree_forest_rec := Induction for tree
-  Sort Set
+Scheme tree_forest_rec := Induction for tree Sort Set
   with forest_tree_rec := Induction for forest Sort Set.
 \end{coq_example*}
 
@@ -316,7 +314,7 @@ We can now prove the following lemma using this principle:
 
 
 \begin{coq_example*}
-Lemma div2_le' : forall n:nat, (div2 n <= n).
+Lemma div2_le' : forall n:nat, div2 n <= n.
 intro n.
  pattern n.
 \end{coq_example*}
@@ -339,7 +337,7 @@ building the principle:
 
 \begin{coq_example*}
 Reset div2_ind.
-Lemma div2_le : forall n:nat, (div2 n <= n).
+Lemma div2_le : forall n:nat, div2 n <= n.
 intro n.
 \end{coq_example*}
 
diff --git a/doc/macros.tex b/doc/macros.tex
index 4ca4869d0..e2b4c20ff 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -94,17 +94,22 @@
 %% New syntax specific entries
 \newcommand{\annotation}{\nterm{annotation}}
 \newcommand{\binder}{\nterm{binder}}
+\newcommand{\binderlet}{\nterm{binderlet}}
 \newcommand{\binderlist}{\nterm{binderlist}}
-\newcommand{\caseitems}{\nterm{caseitems}}
-\newcommand{\caseitem}{\nterm{case\_item}}
-\newcommand{\casetype}{\nterm{casetype}}
+\newcommand{\caseitems}{\nterm{match\_items}}
+\newcommand{\caseitem}{\nterm{match\_item}}
 \newcommand{\eqn}{\nterm{equation}}
+\newcommand{\ifitem}{\nterm{if\_item}}
 \newcommand{\letclauses}{\nterm{letclauses}}
+\newcommand{\params}{\nterm{params}} % vernac
 \newcommand{\returntype}{\nterm{return\_type}}
+\newcommand{\idparams}{\nterm{ident\_with\_params}}
+\newcommand{\statkwd}{\nterm{statement\_keyword}} % vernac
 \newcommand{\termarg}{\nterm{arg}}
 
 \newcommand{\typecstr}{\zeroone{{\tt :} {\term}}}
 
+
 \newcommand{\Fwterm}{\textrm{\textsl{Fwterm}}}
 \newcommand{\Index}{\textrm{\textsl{index}}}
 \newcommand{\abbrev}{\textrm{\textsl{abbreviation}}}
@@ -146,8 +151,6 @@
 \newcommand{\nestedpattern}{\textrm{\textsl{nested\_pattern}}}
 \newcommand{\name}{\textrm{\textsl{name}}}
 \newcommand{\num}{\textrm{\textsl{num}}}
-\newcommand{\params}{\textrm{\textsl{params}}}
-\newcommand{\binderlet}{\textrm{\textsl{binder\_let}}}
 \newcommand{\pattern}{\textrm{\textsl{pattern}}}
 \newcommand{\intropattern}{\textrm{\textsl{intro\_pattern}}}
 \newcommand{\pat}{\textrm{\textsl{pat}}}