MAJ doc/refman

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

3 files changed, 84 insertions, 87 deletions

diff --git a/CHANGES b/CHANGES
index b134073bf3..c1daeecbd3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,7 +10,7 @@ Syntax
 
 - No more support for version 7 syntax and for translation to version 8 syntax.
 - In fixpoints, the { struct ... } annotation is not mandatory any more when 
-  only one of the arguments has an inductive type (doc TODO-JMN)
+  only one of the arguments has an inductive type
 - Added disjunctive patterns in match-with patterns
 - Support for primitive interpretation of string literals
 - Extended support for Unicode ranges
@@ -19,7 +19,7 @@ Vernacular commands
 
 - Added "Print Ltac qualid" to print a user defined tactic.
 - Added "Print Rewrite HintDb" to print the content of a DB used by
-  autorewrite (doc TODO-JMN).
+  autorewrite.
 - Added "Print Canonical Projections".
 - Added "Example" as synonym of "Definition".
 - Added "Proposition" and "Corollary" as extra synonyms of "Lemma".
@@ -75,8 +75,7 @@ Tactics
 - Better support for coercions to Sortclass in tactics expecting type 
   arguments.
 - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses.
-- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
-  (doc TODO-JMN).
+- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns.
 - New introduction pattern "?" for letting Coq choose a name.
 - Added "eassumption".
 - Added option 'using lemmas' to auto, trivial and eauto.
@@ -112,13 +111,13 @@ Extraction
 
 Modules
 
-- Added "Locate Module qualid" to get the full path of a module (doc TODO).
-- Module/Declare Module syntax made more uniform (doc TODO).
+- Added "Locate Module qualid" to get the full path of a module.
+- Module/Declare Module syntax made more uniform.
 - Added syntactic sugar "Declare Module Export/Import" and
-  "Module Export/Import" (doc TODO).
+  "Module Export/Import".
 - Added syntactic sugar "Module M(Export/Import X Y: T)" and
   "Module Type M(Export/Import X Y: T)"
-  (only for interactive definitions) (doc TODO)
+  (only for interactive definitions)
 - Construct "with" generalized to module paths:
    T with (Definition|Module) M1.M2....Mn.l := l' (doc TODO).
 
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 6cc6dd5c70..f480fc0d2c 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -784,9 +784,7 @@ These are synonyms of the {\tt Definition} forms.
 \end{Variants}
 
 \begin{ErrMsgs}
-\item \errindex{In environment {\dots} the term: {\term$_2$} does not have type
-    {\term$_1$}}.\\
-    \texttt{Actually, it has type {\term$_3$}}.
+\item \errindex{Error: The term ``{\term}'' has type "{\type}" while it is expected to have type ``{\type}''}
 \end{ErrMsgs}
 
 \SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
@@ -1210,20 +1208,22 @@ how to introduce infinite objects in Section~\ref{CoFixpoint}.
 %%
 \subsection{Definition of recursive functions}
 
-\subsubsection{\tt Fixpoint {\ident} {\params} {\tt \{struct}
+\subsubsection{Recursive functions over a inductive type}
+
+The command:
+\begin{center}
+  \texttt{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 arguments specified by the binders in
-\params{} % {\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 {\tt forall {\params} {\tt,} \type$_0$}
-and the value is equivalent to {\tt fun {\params} {\tt =>} \term$_0$}.
+  \comindex{Fixpoint}\label{Fixpoint}}
+\end{center}
+allows to define inductive objects using a fixed point construction.
+The meaning of this declaration is to define {\it ident} a recursive
+function with arguments specified by the binders in {\params} 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 {\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 a special argument called the decreasing
@@ -1349,23 +1349,25 @@ 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 Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
- {\tt \{}decrease\_annot{\tt\}} : type$_0$ := \term$_0$.
-}
-\comindex{Function}
-\label{Function}
-
-This \emph{experimental} command can be seen as a generalization of
-{\tt Fixpoint}.  It is actually a wrapper for several ways of defining
-a function \emph{and other useful related objects}, namely: an
-induction principle that reflects the recursive structure of the
-function (see \ref{FunInduction}), and its fixpoint equality (not
-always, see below).  The meaning of this declaration is to define a
-function {\it ident}, similarly to {\tt Fixpoint}. Like in {\tt
-Fixpoint}, the decreasing argument must be given (unless the function
-is not recursive), but it must not necessary be \emph{structurally}
-decreasing. The point of the {\tt
-\{\}} annotation is to name the decreasing argument \emph{and} to
+\subsubsection{A more complex definition of recursive functions}
+
+The \emph{experimental} command 
+\begin{center}
+   \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+     \{decrease\_annot\} : type$_0$ := \term$_0$}
+   \comindex{Function}
+   \label{Function}
+\end{center}
+can be seen as a generalization of {\tt Fixpoint}.  It is actually a
+wrapper for several ways of defining a function \emph{and other useful
+  related objects}, namely: an induction principle that reflects the
+recursive structure of the function (see \ref{FunInduction}), and its
+fixpoint equality (not always, see below).  The meaning of this
+declaration is to define a function {\it ident}, similarly to {\tt
+  Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be
+given (unless the function is not recursive), but it must not
+necessary be \emph{structurally} decreasing. The point of the {\tt
+  \{\}} annotation is to name the decreasing argument \emph{and} to
 describe which kind of decreasing criteria must be used to ensure
 termination of recursive calls.
 
@@ -1442,43 +1444,35 @@ This error happens generally when:
 
 \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples},\ref{FunInduction}}
 
-Depending on the {\tt \{\}} annotation, different definition
+Depending on the {\tt \{$\ldots$\}} annotation, different definition
 mechanisms are used by {\tt Function}. More precise description
 given below.
 
-
-
-\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
- : type$_0$ := \term$_0$.
-\comindex{Function}
-}
-
-Defines the not recursive function \ident\ as if declared with
-\texttt{Definition}.  Three elimination schemes {\tt\ident\_rect},
-{\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the
-documentation of {\tt Inductive} \ref{Inductive}), which reflect the
-pattern matching structure of \term$_0$.
-
-
-\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
- {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
-\comindex{Function}
-}
-
-Defines the structural recursive  function \ident\ as if declared with
-\texttt{Fixpoint}   .  Three   induction   schemes  {\tt\ident\_rect},
-{\tt\ident\_rec}   and  {\tt\ident\_ind}   are   generated  (see   the
-documentation of {\tt  Inductive} \ref{Inductive}), which reflect the
-recursive structure  of \term$_0$. When  there is only  one parameter,
-{\tt \{struct} \ident$_0${\tt\}} can be omitted.
-
-\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
- {\tt \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
-\comindex{Function}}
-
-\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
- {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
-\comindex{Function}}
+\begin{Variants}
+\item \texttt{ Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+    : type$_0$ := \term$_0$}
+
+  Defines the not recursive function \ident\ as if declared with
+  \texttt{Definition}.  Three elimination schemes {\tt\ident\_rect},
+  {\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the
+  documentation of {\tt Inductive} \ref{Inductive}), which reflect the
+  pattern matching structure of \term$_0$.
+
+\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+    {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$}
+  
+  Defines the structural recursive function \ident\ as if declared
+  with \texttt{Fixpoint}.  Three induction schemes {\tt\ident\_rect},
+  {\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the
+  documentation of {\tt Inductive} \ref{Inductive}), which reflect the
+  recursive structure of \term$_0$. When there is only one parameter,
+  {\tt \{struct} \ident$_0${\tt\}} can be omitted.
+  
+\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt
+      \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ :=
+    \term$_0$}
+\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
+ {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$}
 
 Defines a recursive function by well founded recursion. \textbf{The
 module \texttt{Recdef} of the standard library must be loaded for this
@@ -1534,21 +1528,21 @@ subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independe
 %The decreasing argument cannot be dependent of another??
 
 %Exemples faux ici
+\end{Variants}
 
 
+\subsubsection{Recursive functions over co-indcutive types}
 
-
-
-\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} (see
-Section~\ref{CoInductiveTypes} for the definition of {\tt Stream},
-{\tt hd} and {\tt tl}):
+The command:
+\begin{center}
+  \texttt{CoFixpoint {\ident} : \type$_0$ := \term$_0$}
+  \comindex{CoFixpoint}\label{CoFixpoint}
+\end{center}
+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} (see Section~\ref{CoInductiveTypes} for the definition of
+{\tt Stream}, {\tt hd} and {\tt tl}):
 \begin{coq_eval}
 Reset Initial.
 CoInductive Stream : Set :=
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d42969e1ac..bcf8a8ae7b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3137,6 +3137,10 @@ main subgoal excluded.
 %% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and
 %% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}.
 
+\item \texttt{Print Rewrite HintDb {\ident}}
+
+  This command displays all rewrite hints contained in {\ident}.
+
 \end{Variants}
 
 \subsection{Hints and sections