*** empty log message ***

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

5 files changed, 322 insertions, 187 deletions

diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 9d284fa54..6ac29e487 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -15,6 +15,7 @@ correctness. The rules implemented by the typing algorithm are described in
 chapter \ref{Cic}.
 
 \subsection*{About the grammars in the manual}
+\label{BNF-syntax}\index{BNF metasyntax}
 
 Grammars are presented in Backus-Naur form (BNF). Terminal symbols are
 set in {\tt typewriter font}.  In addition, there are special
@@ -56,9 +57,8 @@ are treated as blanks.
 \paragraph{Identifiers and access identifiers}
 
 Identifiers, written {\ident}, are sequences of letters, digits,
-\verb!_! %, \verb!$!
-and \verb!'!, that do not start with a digit or \verb!'!.  That is,
-they are recognized by the following lexical class:
+\verb!_! and \verb!'!, that do not start with a digit or \verb!'!.
+That is, they are recognized by the following lexical class:
 
 \index{ident@\ident}
 \begin{center}
@@ -136,28 +136,34 @@ employed otherwise:
 \begin{tabular}{llllll}
 \verb!_!          &
 \verb!as!         &
+\verb!at!         &
 \verb!cofix!      &
 \verb!else!       &
 \verb!end!        \\
+%
 \verb!exists!     &
 \verb!exists2!    &
 \verb!fix!        &
-\verb!for!        \\
+\verb!for!        &
 \verb!forall!     &
-\verb!fun!        &
-\verb!if!         \\
+\verb!fun!        \\
+%
+\verb!if!         &
+\verb!IF!         &
 \verb!in!         &
 \verb!let!        &
 \verb!match!      &
-\verb!mod!        &
-\verb!return!     &
-\verb!then!       \\
-\verb!using!      &
-\verb!with!       &
-\verb!IF!         &
+\verb!mod!        \\
+%
 \verb!Prop!       &
+\verb!return!     &
 \verb!Set!        &
-\verb!Type!       \\
+\verb!then!       &
+\verb!Type!       &
+\verb!using!      \\
+%
+\verb!where!      &
+\verb!with!       &
 \end{tabular}
 \end{center}
 
@@ -243,31 +249,61 @@ employed otherwise:
 The following sequences of characters are special tokens:
 \begin{center}
 \begin{tabular}{lllllll}
-\verb!(!  &
-\verb!)!  &
-\verb!{!  &
-\verb!}!  &
-\verb!:!  &
-\verb!,!  &
-\verb!|!  \\
-\verb!=>! &
-\verb!->! &
-\verb!:=! &
-\verb!@!  &
-\verb!\%! &
-\verb!.(! &
-\verb!+!  \\
-\verb!-!  &
-\verb!*!  &
-\verb!/!  &
-\verb!=!  &
-\verb!<>! &
-\verb!>!  &
-\verb!<!  \\
-\verb!.!  &
-\verb!;!  &
-\verb!<-! &
-\end{tabular}
+\verb/!/   &
+\verb!%!  &
+\verb!&!   &
+\verb!&&!  &
+\verb!(!   &
+\verb!()!  &
+\verb!)!   \\
+%
+\verb!*!   &
+\verb!+!   &
+\verb!++!  &
+\verb!,!   &
+\verb!-!   &
+\verb!->!  &
+\verb!.!   \\
+%
+\verb!.(!  &
+\verb!..!  &
+\verb!/!   &
+\verb!/\!  &
+\verb!:!   &
+\verb!::!  &
+\verb!:<!  \\
+%
+\verb!:=!  &
+\verb!:>!  &
+\verb!;!   &
+\verb!<!   &
+\verb!<-!  &
+\verb!<->! &
+\verb!<:!  \\
+%
+\verb!<=!  &
+\verb!<>!  &
+\verb!=!   &
+\verb!=>!  &
+\verb!=_D! &
+\verb!>!   &
+\verb!>->! \\
+%
+\verb!>=!  &
+\verb!?!   &
+\verb!?=!  &
+\verb!@!   &
+\verb![!   &
+\verb!\/!  &
+\verb!]!   \\
+%
+\verb!^!   &
+\verb!{!   &
+\verb!|!   &
+\verb!|-!  &
+\verb!||!  &
+\verb!}!   &
+\verb!~!   \\\end{tabular}
 \end{center}
 
 Lexical ambiguities are resolved according to the ``longest match''
@@ -278,51 +314,63 @@ possible one (among all tokens defined at this moment), and so on.
 \section{Terms}\label{term}\index{Terms}
 \subsection{Syntax of terms}
 
-Figure \ref{term-syntax} describes the basic set of terms which form
-the {\em Calculus
-of Inductive Constructions} (also called \CIC). The formal
-presentation of {\CIC} is given in chapter \ref{Cic}. Extensions of
-this syntax are given in chapter
+Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic
+set of terms which form the {\em Calculus of Inductive Constructions}
+(also called \CIC). The formal presentation of {\CIC} is given in
+chapter \ref{Cic}. Extensions of this syntax are given in chapter
 \ref{Gallina-extension}. How to customize the syntax is described in
 chapter \ref{Addoc-syntax}.
 
+\begin{center}
 \begin{figure}[htb]
-\begin{tabular}{|lcl|}
+\begin{tabular}{|lcl@{~~~~~}r|}
 \hline
-{\term} & ::= & {\qualid} \\
-  & $|$ & {\sort} \\
- & $|$ & {\term} {\tt ->} {\term} \\
- & $|$ & {\tt (} {\nelist{\typedidents}{;}} {\tt )} {\term}\\
- & $|$ & {\tt [} {\nelist{\localdecls}{;}} {\tt ]} {\term}\\
- & $|$ & {\tt (} \nelist{\term}{} {\tt )}\\
- & $|$ & {\tt \zeroone{\annotation}} {\tt Cases} {\term} {\tt of}
-        \sequence{\eqn}{|} {\tt end}\\
- & $|$ & {\tt Fix} {\ident} \verb.{. \nelist{\fixpointbody}{with} \verb.}.\\
- & $|$ & {\tt CoFix} {\ident} \verb.{. \nelist{\cofixpointbody}{with} \verb.}.\\
- & & \\
-{\qualid} & ::= & {\ident} \\
- & $|$ & {\qualid} {\accessident} \\
- & & \\
-{\sort} & ::= & {\tt Prop} \\
- & $|$ & {\tt Set} \\
- & $|$ & {\tt Type} \\
- & & \\
-{\annotation} & ::= & \verb!<! {\term} \verb!>!\\
- & & \\
-{\typedidents} & ::= &   \nelist{\ident}{,} {\tt :} {\term}\\
-{\localassums} & ::= &   \nelist{\ident}{,} \zeroone{{\tt :} {\term}}\\
-{\localdef} & ::= & {\ident} {\tt :=} {\term} \zeroone{{\tt :} {\term}}\\
-{\localdecls} & ::= &   \localassums \\
- & $|$ & {\localdef} \\
- & & \\
-{\fixpointbody} & ::= & {\ident} {\tt [} \nelist{\typedidents}{;}  {\tt ]}\verb.:. 
-    {\term} \verb.:=. {\term} \\
-{\cofixpointbody} & ::= & {\ident} \verb.:. 
-    {\term} \verb.:=. {\term} \\
-  & &\\
-{\simplepattern}  & ::= & {\ident} \\
- & $|$ & \verb!(! \nelist{\ident}{} \verb!)! \\
-{\eqn} & ::= &  {\simplepattern} ~\verb!=>! ~\term \\
+{\term} & ::= &
+         {\tt forall} {\binderlist} {\tt ,} {\term}  &(\ref{products})\\
+ & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\
+ & $|$ & {\tt fix} {\fixpointbodies} &(\ref{fixpoints})\\
+ & $|$ & {\tt cofix} {\cofixpointbodies} &(\ref{fixpoints})\\
+ & $|$ & {\tt let} {\letclauses} {\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})\\
+ & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\
+ & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\
+ & $|$ & {\term} \nelist{\termarg}{}&(\ref{applications})\\
+ & $|$ & {\tt @} {\qualid} \sequence{\term}{} &(\ref{applications})\\
+ & $|$ & {\term} {\tt \%} {\ident} &(\ref{scopechange})\\
+ & $|$ & {\tt match} {\caseitems} \zeroone{\casetype} {\tt with} &\\
+    &&   ~~~\zeroone{\zeroone{\tt |} \nelist{\eqn}{|}} {\tt end}
+    &(\ref{caseanalysis})\\
+ & $|$ & {\qualid} &(\ref{qualid})\\
+ & $|$ & {\sort} &(\ref{Gallina-sorts})\\
+ & $|$ & {\num} &(\ref{numerals})\\
+ & $|$ & {\_} &(\ref{applications})\\
+ & & &\\
+{\termarg} & ::= & {\term} &\\
+ & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )} &\\
+ & $|$ & {\tt (} {\num} {\tt :=} {\term} {\tt )} &\\
+&&&\\
+{\binderlist} & ::= & \nelist{\name}{} {\typecstr} &\\
+ & $|$ & {\binder} \nelist{\binderlet}{} &\\
+{\binder} & ::= &   {\name} &\\
+ & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\  
+{\binderlet} & ::= & {\binder} &\\
+ & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\
+& & &\\
+{\qualid} & ::= & {\ident} &\\
+ & $|$ & {\qualid} {\accessident} &\\
+ & & &\\
+{\name} & \cn{}::= & {\ident} &\\
+ & $|$ & {\tt \_} &\\
+&&&\\
+{\sort} & ::= & {\tt Prop} &\\
+ & $|$ & {\tt Set} &\\
+ & $|$ & {\tt Type} &\\
 \hline
 \end{tabular}
 \caption{Syntax of terms}
@@ -330,10 +378,52 @@ chapter \ref{Addoc-syntax}.
 \index{term@{\term}}
 \index{sort@{\sort}}
 \end{figure}
+\end{center}
+
+
+
+\begin{center}
+\begin{figure}[htb]
+\begin{tabular}{|lcl|}
+\hline
+{\fixpointbodies} & ::= &
+         {\fixpointbody} \\
+ & $|$ & {\fixpointbody} {\tt with} \nelist{\fixpointbody}{{\tt with}}
+         {\tt for} {\ident} \\
+{\cofixpointbodies} & ::= &
+         {\cofixpointbody} \\
+ & $|$ & {\cofixpointbody} {\tt with} \nelist{\cofixpointbody}{{\tt with}}
+         {\tt for} {\ident} \\
+&&\\
+{\fixpointbody} & ::= &
+    {\ident} \nelist{\binderlet}{} \zeroone{\annotation} {\typecstr}
+    {\tt :=} {\term} \\
+{\cofixpointbody} & ::= &
+    {\ident} \sequence{\binderlet}{} {\typecstr} {\tt :=} {\term} \\
+  & &\\
+{\annotation} & ::= & {\tt \{ struct} {\ident} {\tt \}} \\ 
+&&\\
+{\caseitems} & ::= & \nelist{\caseitem}{\tt ,} \\
+&&\\
+{\caseitem} & ::= & {\term} \zeroone{{\tt as} \name}
+     \zeroone{{\tt in} \term} \\
+&&\\
+{\casetype} & ::= & {\tt return} {\term} \\
+&&\\
+{\returntype} & ::= & \zeroone{{\tt as} {\name}} {\casetype} \\
+&&\\
+{\eqn} & ::= & \nelist{\pattern}{\tt ,} {\tt =>} {\term}\\
+\hline
+\end{tabular}
+\caption{Syntax of terms (continued)}
+\label{term-syntax-aux}
+\end{figure}
+\end{center}
 
 %%%%%%%
 \subsection{Qualified identifiers and simple identifiers}
-\label{qualid}\label{ident}
+\label{qualid}
+\label{ident}
 
 {\em Qualified identifiers} ({\qualid}) denote {\em global constants}
 (definitions, lemmas, theorems, remarks or facts), {\em global
@@ -343,6 +433,11 @@ types} or {\em constructors of inductive types}.
 syntactic subset of qualified identifiers.  Identifiers may also
 denote local {\em variables}, what qualified identifiers do not.
 
+\subsection{Numerals}
+\label{numerals}
+
+%% TODO
+
 \subsection{Sorts}\index{Sorts}
 \index{Type@{\Type}}
 \index{Set@{\Set}}
@@ -377,48 +472,54 @@ of types inside the syntactic class {\term}.
 \index{type@{\type}}
 
 \subsection{Abstractions}
+\label{abstractions}
 \index{abstractions}
 
-The expression ``{\tt [} {\ident} {\tt :} \type {\tt ]}
-{\term}'' denotes the {\em abstraction} of the variable {\ident}
-of type {\type}, over the term {\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}.
 
-One can abstract several variables successively:
-the notation {\tt [} {\ident$_{1}$} {\tt ,} {\ldots} {\tt ,} 
-{\ident$_{n}$} {\tt :} \type {\tt ]} {\term} stands for 
-{\tt [} {\ident$_{1}$} {\tt :} \type {\tt ](} {\ldots} 
-{\tt ([} {\ident$_{n}$} {\tt :} \type {\tt ]} {\term} {\tt )} 
-\ldots {\tt )} and the notation {\tt [} {\localassums$_{1}$} {\tt ;}
-{\ldots} {\tt ;} {\localassums$_{m}$} {\tt ]} {\term} is a shorthand
-for {\tt [}~{\localassums$_{1}$} {\tt ](} {\ldots} {\tt ([}
-{\localassums$_{m}$} {\tt ]} {\term} {\tt )}.
+One can abstract several variables successively: the 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 may be omitted in an
+\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 brackets mixed with
-assumptions. Obviously, this is expanded into unary abstractions
-separated by let-in's.
+\Rem Local definitions may appear inside parentheses. Obviously, this
+is expanded into a let-in.
 
 
 \subsection{Products}
+\label{products}
 \index{products}
 
-The expression ``{\tt (}~{\ident} {\tt :} \type {\tt )}
-{\term}'' denotes the {\em product} of the variable {\ident}
-of type {\type}, over the term {\term}.
+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 (} {\ident$_{1}$} {\tt ,} {\ldots} {\tt
-,} {\ident$_{n}$} {\tt :} \type {\tt )} {\term} is equivalent to {\tt
-(} {\ident$_{1}$} {\tt :} \type {\tt )(} {\ldots} {\tt ((}
-{\ident$_{n}$} {\tt :} \type {\tt )} {\term} {\tt )} \ldots {\tt )}
-and the expression {\tt (} {\typedidents$_{1}$} {\tt ;} {\ldots} {\tt
-;} {\typedidents$_{m}$} {\tt )} {\term} is a equivalent to {\tt
-(}~{\typedidents$_{1}$} {\tt )(} {\ldots} {\tt ((}
-{\typedidents$_{m}$} {\tt )} {\term} {\tt )} \ldots {\tt )}
+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}
+
+
+Non dependent product types have a special notation ``$A$ {\tt ->}
+$B$'' stands for ``{\tt forall \_:}$A${\tt ,}~$B$''. This is to stress
+on the fact that non dependent produt types are usual functional types.
 
 \subsection{Applications}
+\label{applications}
 \index{applications}
 
 {\tt (}\term$_0$ \term$_1${\tt)} denotes the application of
@@ -430,59 +531,80 @@ 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
+%% \_
+
+
 \subsection{Local definitions (let-in)}
+\label{let-in}
 \index{Local definitions}
 \index{let-in}
 
-{\tt [}{\ident}{\tt :=}{\term$_1$}{\tt ]}{\term$_2$} denotes the local
-binding of \term$_1$ to the variable $\ident$ in \term$_2$.
 
-\medskip
-\Rem The expression {\tt [}{\ident}{\tt :=}{\term$_1$}{\tt
-:}{\type}{\tt ]}{\term$_2$} is an alternative form for the expression {\tt [}{\ident}{\tt
-:=(}{\term$_1$}{\tt ::}{\type}{\tt )]}{\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$.
 
-\Rem An alternative equivalent syntax for let-in is {\tt let} {\ident}
-{\tt =} {\term} {\tt in} {\term}.  For historical reasons, the syntax
-{\tt [} {\ident} {\tt =} {\term} {\tt ]} {\term} is also available but
-is not recommended.
 
 \subsection{Definition by case analysis}
-\index{Cases@{\tt Cases\ldots of\ldots end}}
+\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 \zeroone{\annotation}} {\tt Cases} {\term$_0$} {\tt of}
+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). 
 
-The {\annotation} is the resulting type of the whole {\tt Cases}
+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 Cases} depends on the actual {\term$_0$}
+resulting type of the whole {\tt match} depends on the actual {\term$_0$}
 matched.
 
+%% TODO: variants let (,,) and if/then/else
 
 \subsection{Recursive functions}
-\index{Fix@{Fix \ident$_i$\{\dots\}}}
+\label{fixpoints}
+\index{fix@{fix \ident$_i$\{\dots\}}}
+
+The expression ``{\tt fix} \ident$_1$ \binders$_1$ {\tt :} {\type$_1$}
+\texttt{:=} \term$_1$ {\tt with} {\ldots} {\tt with} \ident$_n$
+\binders$_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.
+
+The expression ``{\tt cofix} \ident$_1$~\binders$_1$ {\tt :}
+{\type$_1$} {\tt with} {\ldots} {\tt with} \ident$_n$ \binders$_n$
+{\tt :} {\type$_n$}~{\tt for} {\ident$_i$}'' denotes the $i$th
+component of a block of terms defined by a mutual guarded recursion.
 
-The expression {\tt Fix} {\ident$_i$} \verb.{. \ident$_1$ {\tt [}
-\binders$_1$ {\tt ] :} {\type$_1$} \texttt{:=} \term$_1$ 
-{\tt with} {\ldots} 
-{\tt with} \ident$_n$ {\tt [} \binders$_n$~{\tt{]} :} {\type$_n$}
-\texttt{:=} \term$_n$ \verb.}. denotes
-the $i$th component of a block of functions defined by mutual
-well-founded recursion.
+The association of a single fixpoint and a local
+definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
+  :=}~{\ldots}~{\tt in}~{\ldots}'' stands for ``{\tt let}~$f$~{\tt :=
+  fix}~$f$~\ldots~{\tt :=}~{\ldots}~{\tt in}~{\ldots}''. The same
+  applies for co-fixpoints.
 
-The expression {\tt CoFix} {\ident$_i$} \verb.{. \ident$_1$
-{\tt :} {\type$_1$} {\tt with} {\ldots} {\tt with}
-\ident$_n$ {\tt [} \binders$_n$ {\tt ] :} {\type$_n$}~\verb.}. denotes
-the $i$th component of a block of terms defined by a mutual guarded recursion. 
+
+\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}
@@ -520,10 +642,10 @@ and ends with a dot.
            & & \\
 
 {\inductive} & ::= & 
- \zeroone{\texttt{Mutual}} {\tt Inductive} \nelist{\inductivebody}{with} 
+ {\tt Inductive} \nelist{\inductivebody}{with} 
     \verb:.: \\
  & $|$ & 
- \zeroone{\texttt{Mutual}} {\tt CoInductive} \nelist{\inductivebody}{with}
+ {\tt CoInductive} \nelist{\inductivebody}{with}
     \verb:.: \\
            & & \\
 {\inductivebody} & ::= & 
@@ -868,13 +990,10 @@ with {\ident$_m$} : {\type$_m$} := \\
 }
 \medskip
 
-\noindent {\bf Remark: } The word {\tt Mutual} can be optionally
-inserted in front of {\tt Inductive}.
-
-It has the same semantics as the above {\tt Inductive} definition for
-each \ident$_1$, {\ldots}, \ident$_m$. All names \ident$_1$, {\ldots},
-\ident$_m$ and \ident$_1^1$, \dots, \ident$_{n_m}^m$ are
-simultaneously added to the environment. Then
+\noindent It has the same semantics as the above {\tt Inductive}
+definition for each \ident$_1$, {\ldots}, \ident$_m$. All names
+\ident$_1$, {\ldots}, \ident$_m$ and \ident$_1^1$, \dots,
+\ident$_{n_m}^m$ are simultaneously added to the environment. Then
 well-typing of constructors can be checked. Each one of the
 \ident$_1$, {\ldots}, \ident$_m$ can be used on its own.
 
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 38ab55515..1a6aa2dab 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -195,10 +195,10 @@ The following abbreviations are allowed:
 \begin{center}
   \begin{tabular}[h]{|l|r|}
     \hline
-    \verb+(exists x:A | P)+     & \verb+(ex A [x:A]P)+ \\
-    \verb+(exists x | P)+       & \verb+(ex A [x:A]P)+ \\
-    \verb+(exists2 x:A | P & Q)+ & \verb+(ex2 A [x:A]P [x:A]Q)+ \\
-    \verb+(exists2 x | P & Q)+   & \verb+(ex2 A [x:A]P [x:A]Q)+ \\
+    \verb+(exists x:A, P)+     & \verb+(ex A [x:A]P)+ \\
+    \verb+(exists x, P)+       & \verb+(ex A [x:A]P)+ \\
+    \verb+(exists2 x:A, P & Q)+ & \verb+(ex2 A [x:A]P [x:A]Q)+ \\
+    \verb+(exists2 x, P & Q)+   & \verb+(ex2 A [x:A]P [x:A]Q)+ \\
     \hline
   \end{tabular}
 \end{center}
diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index 204ec44e2..84ec732fb 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -12,8 +12,6 @@ you can refer to~\cite{Del00}.
 
 \section{Syntax}
 
-\def\nterm#1{\textrm{\textsl{#1}}}
-
 \def\tacexpr{\textrm{\textsl{expr}}}
 \def\tacexprlow{\textrm{\textsl{tacexpr$_1$}}}
 \def\tacexprinf{\textrm{\textsl{tacexpr$_2$}}}
@@ -27,16 +25,17 @@ you can refer to~\cite{Del00}.
 \def\primitivetactic{\textrm{\textsl{primitive\_tactic}}}
 \def\tacarg{\textrm{\textsl{arg}}}
 \def\qstring{\textrm{\textsl{string}}}
-\def\name{\textrm{\textsl{name}}}
+\def\cpattern{\nterm{cpattern}}
 
 The syntax of the tactic language is given in tables~\ref{ltac}
 and~\ref{ltac_aux}. See section~\ref{BNF-syntax} for a description of
 the BNF metasyntax used in these tables. Various already defined
 entries will be used in this chapter: entries {\naturalnumber},
-{\integer}, {\ident}, {\qualid}, {\term}, {\pattern} and
+{\integer}, {\ident}, {\qualid}, {\term}, {\cpattern} and
 {\primitivetactic} represent respectively the natural and integer
 numbers, the authorized identificators and qualified names, {\Coq}'s
-terms and patterns and all the basic tactics. In {\pattern}, there can
+terms and patterns and all the basic tactics. The syntax of
+{\cpattern} is the same as that of terms, but there can
 be specific variables like {\tt ?id} where {\tt id} is a {\ident} or
 {\tt \_}, which are metavariables for pattern matching. {\tt ?id} allows
 us to keep instantiations and to make constraints whereas {\tt \_}
@@ -127,20 +126,17 @@ table~\ref{ltactop}.
 \\
 \contextrule & \cn{}::= &
   \nelist{\contexthyps}{\tt ,} {\tt |-}
-{\pattern} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt |-} {\pattern} {\tt =>} {\tacexpr}\\
+{\cpattern} {\tt =>} {\tacexpr}\\
+& \cn{}| & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
 & \cn{}| & {\tt \_ =>} {\tacexpr}\\
 \\
 \contexthyps & \cn{}::= &
-           {\name} {\tt :} {\pattern}\\
+           {\name} {\tt :} {\cpattern}\\
 \\
 \matchrule & \cn{}::= &
-           {\pattern} {\tt =>} {\tacexpr}\\
-& \cn{}| & {\tt context} {\zeroone{\ident}} {\tt [} {\pattern} {\tt ]} {\tt =>} {\tacexpr}\\
+           {\cpattern} {\tt =>} {\tacexpr}\\
+& \cn{}| & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\
 & \cn{}| & {\tt \_ =>} {\tacexpr}\\
-\\
-\name & \cn{}::= & {\ident} \\
-& \cn{}| & \_
 \end{tabular}
 \end{center}}}
 \caption{Syntax of the tactic language (continued)}
@@ -428,19 +424,19 @@ We can carry out pattern matching on terms with:
 
 \begin{tabular}{l}
 {\tt match} {\tacexpr} {\tt with}\\
-~~~{\pattern}$_1$ {\tt =>} {\tacexpr}$_1$\\
-~{\tt |} {\pattern}$_2$ {\tt =>} {\tacexpr}$_2$\\
+~~~{\cpattern}$_1$ {\tt =>} {\tacexpr}$_1$\\
+~{\tt |} {\cpattern}$_2$ {\tt =>} {\tacexpr}$_2$\\
 ~...\\
-~{\tt |} {\pattern}$_n$ {\tt =>} {\tacexpr}$_n$\\
+~{\tt |} {\cpattern}$_n$ {\tt =>} {\tacexpr}$_n$\\
 ~{\tt |} {\tt \_} {\tt =>} {\tacexpr}$_{n+1}$\\
 {\tt end}
 \end{tabular}
 
 The {\tacexpr} is evaluated and should yield a term which is matched
-(non-linear first order unification) against {\pattern}$_1$ then
+(non-linear first order unification) against {\cpattern}$_1$ then
 {\tacexpr}$_1$ is evaluated into some value by substituting the
 pattern matching instantiations to the metavariables. If the matching
-with {\pattern}$_1$ fails, {\pattern}$_2$ is used and so on.  The
+with {\cpattern}$_1$ fails, {\cpattern}$_2$ is used and so on.  The
 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
@@ -461,9 +457,9 @@ then a no-matching error is raised. \\
 There is a special form of patterns to match a subterm against the
 pattern:\\
 
-{\tt context} {\ident} {\tt [} {\pattern} {\tt ]}\\
+{\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}\\
 
-It matches any term which one subterm matches {\pattern}. If there is
+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
 hole. The definition of {\tt context} in expressions below will show
@@ -484,12 +480,12 @@ We can make pattern matching on goals using the following expression:
 \begin{tabular}{l}
 {\tt match goal with}\\
 ~~~$hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$
-   ~~{\tt |-}{\pattern}$_1${\tt =>} {\tacexpr}$_1$\\
+   ~~{\tt |-}{\cpattern}$_1${\tt =>} {\tacexpr}$_1$\\
 ~~{\tt |}$hyps_{2,1}${\tt ,}...{\tt ,}$hyp_{2,m_2}$
-   ~~{\tt |-}{\pattern}$_2${\tt =>} {\tacexpr}$_2$\\
+   ~~{\tt |-}{\cpattern}$_2${\tt =>} {\tacexpr}$_2$\\
 ~~...\\
 ~~{\tt |}$hyp_{n,1}${\tt ,}...{\tt ,}$hyp_{n,m_n}$
-   ~~{\tt |-}{\pattern}$_n${\tt =>} {\tacexpr}$_n$\\
+   ~~{\tt |-}{\cpattern}$_n${\tt =>} {\tacexpr}$_n$\\
 ~~{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\
 {\tt end}
 \end{tabular}
@@ -498,7 +494,7 @@ We can make pattern matching on goals using the following expression:
 
 If each hypothesis pattern $hyp_{1,i}$, with $i=1,...,m_1$
 is matched (non-linear first order unification) by an hypothesis of
-the goal and if {\pattern}$_1$ is matched by the conclusion of the
+the goal and if {\cpattern}$_1$ is matched by the conclusion of the
 goal, then {\tacexpr}$_1$ is evaluated to $v_1$ by substituting the
 pattern matching to the metavariables and the real hypothesis names
 bound to the possible hypothesis names occurring in the hypothesis
diff --git a/doc/Translator.tex b/doc/Translator.tex
index 02cbdf02e..49c42d080 100644
--- a/doc/Translator.tex
+++ b/doc/Translator.tex
@@ -8,6 +8,10 @@
 \usepackage{pslatex}
 \usepackage{url}
 \usepackage{verbatim}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{array}
+\usepackage{fullpage}
 
 \title{Translation from Coq V7 to V8}
 \author{The Coq Development Team}
@@ -99,7 +103,7 @@ replaced by the general notion of scope.
 \begin{tabular}{l|l|l}
 type & scope name & delimiter \\
 \hline
-types & type_scope & \TERM{T} \\
+types & type_scope & \TERM{type} \\
 \TERM{bool} & bool_scope & \\
 \TERM{nat} & nat_scope & \TERM{nat} \\
 \TERM{Z} & Z_scope & \TERM{Z} \\
@@ -137,17 +141,19 @@ bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{-}$ \\
 list_scope & $\TERM{::} ~\TERM{++}$
 \end{tabular}
 \end{center}
-(Note: $\leq$ is written \TERM{$<=$})
+(Note: $\leq$ stands for \TERM{$<=$})
 
 
 
 \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.
-
+tactics. Argument positions follow the argument names of the head
+constant. The example below assumes \verb+f+ is a function with 2
+dependent arguments named \verb+x+ and \verb+y+, and a third
+non-dependent argument.
 \begin{transbox}
-\TRANS{f 1!t1 2!t2}{f (x:=t1) (y:=t2)}
+\TRANS{f 1!t1 2!t2 3!t3}{f (x:=t1) (y:=t2) (1:=t3)}
 \TRANS{!f t1 t2}{@f t1 t2}
 \end{transbox}
 
@@ -224,8 +230,8 @@ one variable. The type of the result can be omitted if inferable.
 ~~match n with \\~~~~0 => 1 \\~~| (S k) => n * fact k end}
 \end{transbox}
 
-There is a syntactic sugar for mutual fixpoints associated to a local
-definition:
+There is a syntactic sugar for single fixpoints (defining one
+variable) associated to a local definition:
 
 \begin{transbox}
 \TRANS{let f := Fix f \{f [x:A] : T := M\} in\\(g (f y))}{let fix f (x:A) : T := M in\\g (f x)}
@@ -239,7 +245,7 @@ The same applies to cofixpoints, annotations are not allowed in that case.
 \TRANS{O :: nat}{0 : nat}
 \end{transbox}
 
-\section{Main changes in tactics w.r.t. V7}
+\subsection{Main changes in tactics w.r.t. V7}
 
 The main change is that all tactic names are lowercase. This also holds for
 Ltac keywords.
@@ -259,7 +265,7 @@ became \TERM{context}. Syntax is unified with subterm matching.
 \TRANS{match t with [C[x=y]] => inst C[y=x]}{match t with context C[x=y] => context C[y=x]}
 \end{transbox}
 
-\subsubsection{Named arguments of theorems}
+\subsubsection{Named arguments of theorems ({\em bindings})}
 
 \begin{transbox}
 \TRANS{Apply thm with x:=t 1:=u}{apply thm with (x:=t) (1:=u)}
@@ -270,7 +276,8 @@ became \TERM{context}. Syntax is unified with subterm matching.
 
 To avoid ambiguity between a numeric literal and the optionnal
 occurence numbers of this term, the occurence numbers are put after
-the term itself. This applies to tactic \TERM{pattern} and also
+the term itself and after keyword \TERM{as}. This applies to tactic
+\TERM{pattern} and also
 \TERM{unfold}
 \begin{transbox}
 \TRANS{Pattern 1 2 (f x) 3 4 d y z}{pattern (f x at 1 2) (d at 3 4) y z}
@@ -317,7 +324,7 @@ 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/check-v8} will help translate developments that
+\item {\tt tools/translate-v8} will help translate developments that
 compile with a Makefile with minimum requirements.
 \end{itemize}
 
@@ -335,10 +342,10 @@ by {\tt coq\_makefile}, you probably just have to do
 When the development compiles successfully, there are several changes
 that might be necessary for the translation. Essentially, this is
 about syntax extensions (see section below dedicated to porting syntax
-extensions). If you do not use such features, then you can try and
-make the translation.
+extensions). If you do not use such features, then you are ready to
+try and make the translation.
 
-The preferred way is to use script {\tt check-v8} if your development
+The preferred way is to use script {\tt translate-v8} if your development
 is compiled by a Makfile with the following constraints:
 \begin{itemize}
 \item compilation is achievd by invoke make without arguments
diff --git a/doc/macros.tex b/doc/macros.tex
index 080aeb77a..02a29458a 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -85,19 +85,30 @@
 % \rm\sl series %
 %%%%%%%%%%%%%%%%%
 
+\newcommand{\nterm}[1]{\textrm{\textsl{#1}}}
+
+%% New syntax specific entries
+\newcommand{\termarg}{\nterm{arg}}
+\newcommand{\caseitems}{\nterm{caseitems}}
+\newcommand{\caseitem}{\nterm{case\_item}}
+\newcommand{\casetype}{\nterm{casetype}}
+\newcommand{\letclauses}{\nterm{letclauses}}
+\newcommand{\annotation}{\nterm{annotation}}
+\newcommand{\returntype}{\nterm{return\_type}}
+
+\newcommand{\typecstr}{\zeroone{{\tt :} {\term}}}
+
 \newcommand{\Fwterm}{\textrm{\textsl{Fwterm}}}
 \newcommand{\Index}{\textrm{\textsl{index}}}
 \newcommand{\abbrev}{\textrm{\textsl{abbreviation}}}
-\newcommand{\annotation}{\textrm{\textsl{annotation}}}
-\newcommand{\returntype}{\textrm{\textsl{return\_type}}}
-\newcommand{\caseitem}{\textrm{\textsl{case\_item}}}
 \newcommand{\atomictac}{\textrm{\textsl{atomic\_tactic}}}
 \newcommand{\binders}{\textrm{\textsl{bindings}}}
 \newcommand{\binder}{\textrm{\textsl{binding}}}
+\newcommand{\binderlist}{\nterm{binderlist}}
 \newcommand{\bindinglist}{\textrm{\textsl{bindings\_list}}}
 \newcommand{\cast}{\textrm{\textsl{cast}}}
+\newcommand{\cofixpointbodies}{\textrm{\textsl{cofix\_bodies}}}
 \newcommand{\cofixpointbody}{\textrm{\textsl{cofix\_body}}}
-\newcommand{\coinductivebody}{\textrm{\textsl{coind\_body}}}
 \newcommand{\commandtac}{\textrm{\textsl{tactic\_invocation}}}
 \newcommand{\constructor}{\textrm{\textsl{constructor}}}
 \newcommand{\convtactic}{\textrm{\textsl{conv\_tactic}}}
@@ -110,6 +121,7 @@
 \newcommand{\field}{\textrm{\textsl{field}}}
 \newcommand{\firstletter}{\textrm{\textsl{first\_letter}}}
 \newcommand{\fixpg}{\textrm{\textsl{fix\_pgm}}}
+\newcommand{\fixpointbodies}{\textrm{\textsl{fix\_bodies}}}
 \newcommand{\fixpointbody}{\textrm{\textsl{fix\_body}}}
 \newcommand{\fixpoint}{\textrm{\textsl{fixpoint}}}
 \newcommand{\flag}{\textrm{\textsl{flag}}}
@@ -129,6 +141,7 @@
 \newcommand{\mutualcoinductive}{\textrm{\textsl{mutual\_coinductive}}}
 \newcommand{\mutualinductive}{\textrm{\textsl{mutual\_inductive}}}
 \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}}}