Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2

20 files changed, 1125 insertions, 365 deletions

diff --git a/doc/Makefile b/doc/Makefile
index fd508e07..6209b0c8 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -110,7 +110,7 @@ REFMANCOQTEXFILES=\
   refman/RefMan-mod.v.tex refman/RefMan-tac.v.tex \
   refman/RefMan-cic.v.tex refman/RefMan-lib.v.tex \
   refman/RefMan-tacex.v.tex refman/RefMan-syn.v.tex \
-  refman/RefMan-oth.v.tex \
+  refman/RefMan-oth.v.tex refman/RefMan-ltac.v.tex \
   refman/Cases.v.tex refman/Coercion.v.tex refman/Extraction.v.tex \
   refman/Program.v.tex refman/Omega.v.tex refman/Polynom.v.tex \
   refman/Setoid.v.tex refman/Helm.tex # refman/Natural.v.tex
@@ -119,7 +119,7 @@ REFMANTEXFILES=\
   refman/headers.tex \
   refman/Reference-Manual.tex refman/RefMan-pre.tex \
   refman/RefMan-int.tex refman/RefMan-pro.tex \
-  refman/RefMan-com.tex refman/RefMan-ltac.tex \
+  refman/RefMan-com.tex \
   refman/RefMan-uti.tex refman/RefMan-ide.tex \
   refman/RefMan-add.tex refman/RefMan-modr.tex \
   $(REFMANCOQTEXFILES) \
@@ -161,9 +161,15 @@ refman/html/index.html: refman/Reference-Manual.html $(REFMANPNGFILES) \
 	mkdir refman/html
 	cp $(REFMANPNGFILES) refman/html
 	(cd refman/html; hacha -o toc.html ../Reference-Manual.html)
-	cp refman/cover.html refman/html
+	cp refman/cover.html refman/menu.html refman/html
 	cp refman/index.html refman/html
 
+refman-quick:
+	(cd refman; \
+	 $(PDFLATEX) Reference-Manual.tex; \
+	 hevea -fix -exec xxdate.exe ./Reference-Manual.tex)
+
+
 ######################################################################
 # Tutorial
 ######################################################################
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 393b8547..2465d70f 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -161,6 +161,7 @@
 \newcommand{\form}{\textrm{\textsl{form}}}
 \newcommand{\entry}{\textrm{\textsl{entry}}} 
 \newcommand{\proditem}{\textrm{\textsl{production\_item}}} 
+\newcommand{\taclevel}{\textrm{\textsl{tactic\_level}}}
 \newcommand{\tacargtype}{\textrm{\textsl{tactic\_argument\_type}}} 
 \newcommand{\scope}{\textrm{\textsl{scope}}} 
 \newcommand{\optscope}{\textrm{\textsl{opt\_scope}}} 
@@ -182,6 +183,7 @@
 \newcommand{\name}{\textrm{\textsl{name}}}
 \newcommand{\num}{\textrm{\textsl{num}}}
 \newcommand{\pattern}{\textrm{\textsl{pattern}}}
+\newcommand{\orpattern}{\textrm{\textsl{or\_pattern}}}
 \newcommand{\intropattern}{\textrm{\textsl{intro\_pattern}}}
 \newcommand{\pat}{\textrm{\textsl{pat}}}
 \newcommand{\pgs}{\textrm{\textsl{pgms}}}
@@ -200,6 +202,7 @@
 \newcommand{\str}{\textrm{\textsl{string}}}
 \newcommand{\subsequentletter}{\textrm{\textsl{subsequent\_letter}}}
 \newcommand{\switch}{\textrm{\textsl{switch}}}
+\newcommand{\messagetoken}{\textrm{\textsl{message\_token}}}
 \newcommand{\tac}{\textrm{\textsl{tactic}}}
 \newcommand{\terms}{\textrm{\textsl{terms}}}
 \newcommand{\term}{\textrm{\textsl{term}}}
@@ -488,7 +491,7 @@
         {\begin{center}\begin{rulebox}}
         {\end{rulebox}\end{center}}
 
-% $Id: macros.tex 8606 2006-02-23 13:58:10Z herbelin $ 
+% $Id: macros.tex 9038 2006-07-11 13:53:53Z herbelin $ 
 
 
 %%% Local Variables: 
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index a05231cd..dfe9e94c 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -1,5 +1,5 @@
 \achapter{Extended pattern-matching}\defaultheaders
-\aauthor{Cristina Cornes}
+\aauthor{Cristina Cornes and Hugo Herbelin}
 
 \label{Mult-match-full}
 \ttindex{Cases}
@@ -17,32 +17,38 @@ 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
-{\em simple}: it is the kind of pattern recognized by the basic
-version of {\tt match}. If a pattern is
-not simple we call it {\em nested}.
+symbol and $\vec{x}$ is a linear vector of (distinct) variables, it is
+called {\em simple}: it is the kind of pattern recognized by the basic
+version of {\tt match}. On the opposite, if it is a variable $x$ or
+has the form $(c~\vec{p})$ with $p$ not only made of variables, the
+pattern is called {\em nested}.
 
 A variable pattern matches any value, and the identifier is bound to
 that value. The pattern ``\texttt{\_}'' (called ``don't care'' or
-``wildcard'' symbol) also matches any value, but does not bind anything. It
-may occur an arbitrary number of times in a pattern. Alias patterns
-written \texttt{(}{\sl pattern} \texttt{as} {\sl identifier}\texttt{)} are
-also accepted. This pattern matches the same values as {\sl pattern}
-does and {\sl identifier} is bound to the matched value.  A list of
-patterns separated with commas 
-is also considered as a pattern and is called {\em multiple
-pattern}.
+``wildcard'' symbol) also matches any value, but does not bind
+anything. It may occur an arbitrary number of times in a
+pattern. Alias patterns written \texttt{(}{\sl pattern} \texttt{as}
+{\sl identifier}\texttt{)} are also accepted. This pattern matches the
+same values as {\sl pattern} does and {\sl identifier} is bound to the
+matched value.  
+A pattern of the form {\pattern}{\tt |}{\pattern} is called
+disjunctive. A list of patterns separated with commas is also
+considered as a pattern and is called {\em multiple pattern}. However
+multiple patterns can only occur at the root of pattern-matching
+equations. Disjunctions of {\em multiple pattern} are allowed though.
 
 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
-to see the result of the expansion is by printing the term with
-\texttt{Print} if the term is a constant, or using the command
+stage of parsing has finished only simple patterns remain.  Re-nesting
+of pattern is performed at printing time. An easy way to see the
+result of the expansion is to toggle off the nesting performed at
+printing (use here {\tt Set Printing Matching}), then by printing the term
+with \texttt{Print} if the term is a constant, or using the command
 \texttt{Check}.
 
 The extended \texttt{match} still accepts an optional {\em elimination
 predicate} given after the keyword \texttt{return}.  Given a pattern
-matching expression, if all the right hand sides of \texttt{=>} ({\em
+matching expression, if all the right-hand-sides of \texttt{=>} ({\em
 rhs} in short) have the same type, then this type can be sometimes
 synthesized, and so we can omit the \texttt{return} part. Otherwise 
 the predicate after \texttt{return} has to be provided, like for the basic
@@ -64,7 +70,9 @@ Fixpoint max (n m:nat) {struct m} : nat :=
   end.
 \end{coq_example}
 
-Using multiple patterns in the definition allows to write:
+\paragraph{Multiple patterns}
+
+Using multiple patterns in the definition of {\tt max} allows to write:
 
 \begin{coq_example}
 Reset max.
@@ -89,7 +97,9 @@ Check (fun x:nat => match x return nat with
                     end).
 \end{coq_example}
 
-We can also use ``\texttt{as} patterns'' to associate a name to a
+\paragraph{Aliasing subpatterns}
+
+We can also use ``\texttt{as} {\ident}'' to associate a name to a
 sub-pattern:
 
 \begin{coq_example}
@@ -102,6 +112,8 @@ Fixpoint max (n m:nat) {struct n} : nat :=
   end.
 \end{coq_example}
 
+\paragraph{Nested patterns}
+
 Here is now an example of nested patterns:
 
 \begin{coq_example}
@@ -157,7 +169,6 @@ Fixpoint lef (n m:nat) {struct m} : bool :=
   end.
 \end{coq_example}
 
-
 Here the last pattern superposes with the first two. Because
 of the priority rule, the last pattern 
 will be used only for values that do not match neither the  first nor
@@ -180,12 +191,50 @@ Check (fun x:nat =>
          end).
 \end{coq_example}
 
+\paragraph{Disjunctive patterns}
+
+Multiple patterns that share the same right-hand-side can be
+factorized using the notation \nelist{\multpattern}{\tt |}. For instance,
+{\tt max} can be rewritten as follows:
+
+\begin{coq_eval}
+Reset max.
+\end{coq_eval}
+\begin{coq_example}
+Fixpoint max (n m:nat) {struct m} : nat :=
+  match n, m with
+  | S n', S m' => S (max n' m')
+  | 0, p | p, 0 => p
+  end.
+\end{coq_example}
+
+Similarly, factorization of (non necessary multiple) patterns
+that share the same variables is possible by using the notation
+\nelist{\pattern}{\tt |}. Here is an example:
+
+\begin{coq_example}
+Definition filter_2_4 (n:nat) : nat :=
+  match n with
+  | 2 as m | 4 as m => m
+  | _ => 0
+  end.
+\end{coq_example}
+
+Here is another example using disjunctive subpatterns.
+
+\begin{coq_example}
+Definition filter_some_square_corners (p:nat*nat) : nat*nat :=
+  match p with
+  | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n)
+  | _ => (0,0)
+  end.
+\end{coq_example}
+
 \asection{About patterns of parametric types}
 When matching objects of a parametric type, constructors in patterns
 {\em do not expect} the parameter arguments. Their value is deduced
 during expansion.
-
-Consider for example the polymorphic lists:
+Consider for example the type of polymorphic lists:
 
 \begin{coq_example}
 Inductive List (A:Set) : Set :=
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index e288cdfb..0a2f5904 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -218,10 +218,10 @@ either an assumption, written $x:T$ ($T$ is a type) or a definition,
 written $x:=t:T$.  We use brackets to write contexts. A
 typical example is $[x:T;y:=u:U;z:V]$.  Notice that the variables
 declared in a context must be distinct. If $\Gamma$ declares some $x$,
-we write $x \in\Gamma$. By writing $(x:T)\in\Gamma$ we mean that
+we write $x \in \Gamma$. By writing $(x:T) \in \Gamma$ we mean that
 either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such
 that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some
-$x:=t:T$, we also write $(x:=t:T)\in\Gamma$.  Contexts must be
+$x:=t:T$, we also write $(x:=t:T) \in \Gamma$.  Contexts must be
 themselves {\em well formed}.  For the rest of the chapter, the
 notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the context
 $\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The
@@ -233,8 +233,8 @@ notation $[]$ denotes the empty context.  \index{Context}
 
 We define the inclusion of two contexts $\Gamma$ and $\Delta$ (written
 as $\Gamma \subset \Delta$) as the property, for all variable $x$,
-type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T)\in \Delta$
-and if $(x:=t:T) \in \Gamma$ then $(x:=t:T)\in \Delta$.  
+type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$
+and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$.  
 %We write
 % $|\Delta|$ for the length of the context $\Delta$, that is for the number
 % of declarations (assumptions or definitions) in $\Delta$.
@@ -288,28 +288,30 @@ be derived from the following rules.
 \begin{description}
 \item[W-E] \inference{\WF{[]}{[]}}
 \item[W-S]  % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma
-\inference{\frac{\WTEG{T}{s}~~~~s\in \Sort~~~~x \not\in
+\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~x \not\in
       \Gamma           % \cup E
       }
       {\WFE{\Gamma::(x:T)}}~~~~~
     \frac{\WTEG{t}{T}~~~~x \not\in
       \Gamma           % \cup E
      }{\WFE{\Gamma::(x:=t:T)}}}
-\item[Def] \inference{\frac{\WTEG{t}{T}~~~c \notin E\cup \Gamma}
+\item[Def] \inference{\frac{\WTEG{t}{T}~~~c \notin E \cup \Gamma}
                       {\WF{E;\Def{\Gamma}{c}{t}{T}}{\Gamma}}}
+\item[Assum] \inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~c \notin E \cup \Gamma}
+                      {\WF{E;\Assum{\Gamma}{c}{T}}{\Gamma}}}
 \item[Ax] \index{Typing rules!Ax}
 \inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(p)}}~~~~~
 \frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(q)}}}
 \inference{\frac{\WFE{\Gamma}~~~~i<j}{\WTEG{\Type(i)}{\Type(j)}}}
 \item[Var]\index{Typing rules!Var}
- \inference{\frac{ \WFE{\Gamma}~~~~~(x:T)\in\Gamma~~\mbox{or}~~(x:=t:T)\in\Gamma~\mbox{for some $t$}}{\WTEG{x}{T}}}
+ \inference{\frac{ \WFE{\Gamma}~~~~~(x:T) \in \Gamma~~\mbox{or}~~(x:=t:T) \in \Gamma~\mbox{for some $t$}}{\WTEG{x}{T}}}
 \item[Const]  \index{Typing rules!Const}
-\inference{\frac{\WFE{\Gamma}~~~~(c:T) \in E}{\WTEG{c}{T}}}
+\inference{\frac{\WFE{\Gamma}~~~~(c:T) \in E~~\mbox{or}~~(c:=t:T) \in E~\mbox{for some $t$} }{\WTEG{c}{T}}}
 \item[Prod]  \index{Typing rules!Prod}
 \inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~
     \WTE{\Gamma::(x:T)}{U}{\Prop}}
       { \WTEG{\forall~x:T,U}{\Prop}}} 
-\inference{\frac{\WTEG{T}{s}~~~~s\in\{\Prop, \Set\}~~~~~~
+\inference{\frac{\WTEG{T}{s}~~~~s \in\{\Prop, \Set\}~~~~~~
     \WTE{\Gamma::(x:T)}{U}{\Set}}
       { \WTEG{\forall~x:T,U}{\Set}}} 
 \inference{\frac{\WTEG{T}{\Type(i)}~~~~i\leq k~~~
@@ -373,7 +375,7 @@ environment. It is legal to identify such a reference with its value,
 that is to expand (or unfold) it into its value. This
 reduction is called $\delta$-reduction and shows as follows.
 
-$$\WTEGRED{x}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(x:=t:T)\in\Gamma$}~~~~~~~~~\WTEGRED{c}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(c:=t:T)\in E$}$$
+$$\WTEGRED{x}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(x:=t:T) \in \Gamma$}~~~~~~~~~\WTEGRED{c}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(c:=t:T) \in E$}$$
 
 
 \paragraph{$\zeta$-reduction.}
@@ -553,15 +555,13 @@ represented by:
   \List}\]
  Assuming 
   $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
-  $[c_1:C_1;\ldots;c_n:C_n]$, the general typing rules are:
+  $[c_1:C_1;\ldots;c_n:C_n]$, the general typing rules are, 
+  for $1\leq j\leq k$ and $1\leq i\leq n$:
 
 \bigskip
-\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E
-    ~~j=1\ldots k}{(I_j:A_j) \in E}}
+\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E}{(I_j:A_j) \in E}}
 
-\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E
-    ~~~~i=1.. n}
-   {(c_i:C_i)\in E}}
+\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E}{(c_i:C_i) \in E}}
 
 \subsubsection{Inductive definitions with parameters}
 
@@ -593,11 +593,11 @@ p_1:P_1,\ldots,\forall p_r:P_r,\forall a_1:A_1, \ldots \forall a_n:A_n,
 with $I$ one of the inductive definitions in $\Gamma_I$. 
 We say that $n$ is the number of real arguments of the constructor
 $c$. 
-\paragraph{Context of parameters}
+\paragraph{Context of parameters.}
 If an inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits 
 $r$ inductive parameters, then there exists a context $\Gamma_P$ of
-size $r$, such that $\Gamma_P=p_1:P_1;\ldots;\forall p_r:P_r$ and 
-if $(t:A)\in\Gamma_I,\Gamma_C$ then $A$ can be written as 
+size $r$, such that $\Gamma_P=p_1:P_1;\ldots;p_r:P_r$ and 
+if $(t:A) \in \Gamma_I,\Gamma_C$ then $A$ can be written as 
 $\forall p_1:P_1,\ldots \forall p_r:P_r,A'$. 
 We call $\Gamma_P$ the context of parameters of the inductive
 definition and use the notation $\forall \Gamma_P,A'$ for the term $A$.
@@ -741,7 +741,7 @@ contains an inductive declaration.
 
 \inference{\frac{\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E
     ~~~~i=1.. n}
-   {(c_i:C_i)\in E}}
+   {(c_i:C_i) \in E}}
 \end{description}
 
 \paragraph{Example.}
@@ -848,16 +848,16 @@ inductive definition.
 \begin{description}
 \item[W-Ind] Let $E$ be an environment and
   $\Gamma,\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that
-  $\Gamma_I$ is $[I_1:\forall \Gamma_p,A_1;\ldots;I_k:\forall
+  $\Gamma_I$ is $[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall
   \Gamma_P,A_k]$ and $\Gamma_C$ is 
-  $[c_1:\forall \Gamma_p,C_1;\ldots;c_n:\forall \Gamma_p,C_n]$. 
+  $[c_1:\forall \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$. 
 \inference{
   \frac{
   (\WTE{\Gamma;\Gamma_P}{A_j}{s'_j})_{j=1\ldots  k}
   ~~ (\WTE{\Gamma;\Gamma_I;\Gamma_P}{C_i}{s_{p_i}})_{i=1\ldots  n}
 }
   {\WF{E;\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
-providing the following side conditions hold:
+provided that the following side conditions hold:
 \begin{itemize}
 \item $k>0$, $I_j$, $c_i$ are different names for $j=1\ldots  k$ and $i=1\ldots  n$,
 \item $p$ is the number of parameters of \NInd{\Gamma}{\Gamma_I}{\Gamma_C}
@@ -874,7 +874,7 @@ arity of the inductive type and the sort of the type of its
 constructors which will always be satisfied for the impredicative sort
 (\Prop) but may fail to define inductive definition 
 on sort \Set{} and generate constraints between universes for
-inductive definitions in types.
+inductive definitions in the {\Type} hierarchy.
 
 \paragraph{Examples.}
 It is well known that existential quantifier can be encoded as an
@@ -907,6 +907,135 @@ Inductive exType (P:Type->Prop) : Type
 %is recursive or not.  We shall write the type $(x:_R T)C$ if it is 
 %a recursive argument and $(x:_P T)C$ if the argument is not recursive.
 
+\paragraph{Sort-polymorphism of inductive families.}
+\index{Sort-polymorphism of inductive families}
+
+From {\Coq} version 8.1, inductive families declared in {\Type} are
+polymorphic over their arguments in {\Type}.
+
+If $A$ is an arity and $s$ a sort, we write $A_{/s}$ for the arity
+obtained from $A$ by replacing its sort with $s$. Especially, if $A$
+is well-typed in some environment and context, then $A_{/s}$ is typable
+by typability of all products in the Calculus of Inductive Constructions.
+The following typing rule is added to the theory.
+
+\begin{description}
+\item[Ind-Family] Let $\Gamma_P$ be a context of parameters
+$[p_1:P_1;\ldots;p_{m'}:P_{m'}]$ and $m\leq m'$ be the length of the
+initial prefix of parameters that occur unchanged in the recursive
+occurrences of the constructor types. Assume that $\Gamma_I$ is
+$[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ and
+$\Gamma_C$ is $[c_1:\forall \Gamma_P,C_1;\ldots;c_n:\forall
+\Gamma_P,C_n]$.
+
+Let $q_1$, \ldots, $q_r$, with $0\leq r\leq m$, be a possibly partial
+instantiation of the parameters in $\Gamma_P$. We have:
+
+\inference{\frac
+{\left\{\begin{array}{l}
+\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E\\
+(E[\Gamma] \vdash q_s : P'_s)_{s=1\ldots r}\\
+(E[\Gamma] \vdash \WTEGLECONV{P'_s}{\subst{P_s}{x_u}{q_u}_{u=1\ldots s-1}})_{s=1\ldots r}\\
+1 \leq j \leq k
+\end{array}
+\right.}
+{(I_j\,q_1\,\ldots\,q_r:\forall \Gamma^{r+1}_p, (A_j)_{/s})}
+}
+
+provided that the following side conditions hold:
+
+\begin{itemize}
+\item $\Gamma_{P'}$ is the context obtained from $\Gamma_P$ by
+replacing, each $P_s$ that is an arity with the
+sort of $P'_s$, as soon as $1\leq s \leq r$ (notice that
+$P_s$ arity implies $P'_s$ arity since $E[\Gamma]
+\vdash \WTEGLECONV{P'_s}{ \subst{P_s}{x_u}{q_u}_{u=1\ldots s-1}}$);
+\item there are sorts $s_i$, for $1 \leq i \leq k$ such that, for
+ $\Gamma_{I'}$ obtained from $\Gamma_I$ by changing each $A_i$ by $(A_i)_{/s_i}$,
+we have $(\WTE{\Gamma;\Gamma_{I'};\Gamma_{P'}}{C_i}{s_{p_i}})_{i=1\ldots  n}$;
+\item the sorts are such that all elimination are allowed (see
+section~\ref{elimdep}).
+\end{itemize}
+\end{description}
+
+Notice that if $I_j\,q_1\,\ldots\,q_r$ is typable using the rules {\bf
+Ind-Const} and {\bf App}, then it is typable using the rule {\bf
+Ind-Family}. Conversely, the extended theory is not stronger than the
+theory without {\bf Ind-Family}. We get an equiconsistency result by
+mapping each $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$ occurring into a
+given derivation into as many fresh inductive types and constructors
+as the number of different (partial) replacements of sorts, needed for
+this derivation, in the parameters that are arities. That is, the
+changes in the types of each partial instance $q_1\,\ldots\,q_r$ can
+be characterized by the ordered sets of arity sorts among the types of
+parameters, and to each signature is associated a new inductive
+definition with fresh names. Conversion is preserved as any (partial)
+instance $I_j\,q_1\,\ldots\,q_r$ or $C_i\,q_1\,\ldots\,q_r$ is mapped
+to the names chosen in the specific instance of
+$\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$.
+
+\newcommand{\Single}{\mbox{\textsf{Set}}}
+
+In practice, the rule is used by {\Coq} only with in case the
+inductive type is declared with an arity of a sort in the $\Type$
+hierarchy, and, then, the polymorphism is over the parameters whose
+type is an arity in the {\Type} hierarchy. The sort $s_j$ are then
+chosen canonically so that each $s_j$ is minimal with respect to the
+hierarchy ${\Prop_u}\subset{\Set_p}\subset\Type$ where $\Set_p$ is
+predicative {\Set}, and ${\Prop_u}$ is the sort of small singleton
+inductive types (i.e. of inductive types with one single constructor
+and that contains either proofs or inhabitants of singleton types
+only). More precisely, a small singleton inductive family is set in
+{\Prop}, a small non singleton inductive family is set in {\Set} (even
+in case {\Set} is impredicative -- see section~\ref{impredicativity}),
+and otherwise in the {\Type} hierarchy.
+% TODO: clarify the case of a partial application ??
+
+Note that the side-condition about allowed elimination sorts in the
+rule~{\bf Ind-Family} is just to avoid to recompute the allowed
+elimination sorts at each instance of a pattern-matching (see
+section~\ref{elimdep}).
+
+As an example, let us consider the following definition:
+\begin{coq_example*}
+Inductive option (A:Type) : Type := 
+| None : option A 
+| Some : A -> option A.
+\end{coq_example*}
+
+As the definition is set in the {\Type} hierarchy, it is used
+polymorphically over its parameters whose types are arities of a sort
+in the {\Type} hierarchy. Here, the parameter $A$ has this property,
+hence, if \texttt{option} is applied to a type in {\Set}, the result is
+in {\Set}. Note that if \texttt{option} is applied to a type in {\Prop},
+then, the result is not set in \texttt{Prop} but in \texttt{Set}
+still. This is because \texttt{option} is not a singleton type (see
+section~\ref{singleton}) and it would loose the elimination to {\Set} and
+{\Type} if set in {\Prop}.
+
+\begin{coq_example}
+Check (fun A:Set => option A).
+Check (fun A:Prop => option A).
+\end{coq_example}
+
+Here is another example.
+
+\begin{coq_example*}
+Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
+\end{coq_example*}
+
+As \texttt{prod} is a singleton type, it will be in {\Prop} if applied
+twice to propositions, in {\Set} if applied twice to at least one type
+in {\Set} and none in {\Type}, and in {\Type} otherwise. In all cases,
+the three kind of eliminations schemes are allowed.
+
+\begin{coq_example}
+Check (fun A:Set => prod A).
+Check (fun A:Prop => prod A A).
+Check (fun (A:Prop) (B:Set) => prod A B).
+Check (fun (A:Type) (B:Prop) => prod A B).
+\end{coq_example}
+
 \subsection{Destructors}
 The specification of inductive definitions with arities and
 constructors is quite natural.  But we still have to say how to use an
@@ -1049,6 +1178,7 @@ compact notation~:
 %  \mbox{\tt =>}~ \false}
 
 \paragraph{Allowed elimination sorts.}
+
 \index{Elimination sorts}
 
 An important question for building the typing rule for \kw{match} is
@@ -1158,6 +1288,7 @@ the two projections on this type.
 %{\tt Program} tactic or when extracting ML programs.
 
 \paragraph{Empty and singleton elimination}
+\label{singleton}
 \index{Elimination!Singleton elimination}
 \index{Elimination!Empty elimination}
 
@@ -1167,7 +1298,7 @@ eliminations are allowed.
 \item[\Prop-extended] 
 \inference{
    \frac{I \mbox{~is an empty or singleton
-       definition}~~~s\in\Sort}{\compat{I:\Prop}{I\ra s}}
+       definition}~~~s \in \Sort}{\compat{I:\Prop}{I\ra s}}
 }
 \end{description}
 
@@ -1530,7 +1661,7 @@ The major change in the theory concerns the rule for product formation
 in the sort \Set, which is extended to a domain in any sort~:
 \begin{description}
 \item [Prod]  \index{Typing rules!Prod (impredicative Set)}
-\inference{\frac{\WTEG{T}{s}~~~~s\in\Sort~~~~~~
+\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~~~
     \WTE{\Gamma::(x:T)}{U}{\Set}}
       { \WTEG{\forall~x:T,U}{\Set}}} 
 \end{description}
@@ -1553,7 +1684,7 @@ impredicative system for sort \Set{} become~:
      
 
 
-% $Id: RefMan-cic.tex 8914 2006-06-07 14:57:22Z cpaulin $ 
+% $Id: RefMan-cic.tex 9001 2006-07-04 13:50:15Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index f8a7546f..8c54e0ed 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -86,6 +86,7 @@ you move the \Coq\ binaries and library after installation.
 
 \section{Options}
 \index{Options of the command line}
+\label{vmoption}
 
 The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
@@ -239,6 +240,11 @@ The following command-line options are recognized by the commands {\tt
   resulting in a smaller memory requirement and faster compilation;
   warning: this invalidates some features such as the extraction tool.
 
+\item[{\tt -vm}]\ 
+
+  This activates the use of the bytecode-based conversion algorithm
+  for the current session (see section~\ref{SetVirtualMachine}).
+
 \item[{\tt -image} {\em file}]\ 
 
   This option sets the binary image to be used to be {\em file}
@@ -272,7 +278,7 @@ The following command-line options are recognized by the commands {\tt
 %   (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}).
 % \end{description}
 
-% $Id: RefMan-com.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ 
+% $Id: RefMan-com.tex 9044 2006-07-12 13:22:17Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 503d7571..37660aa3 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -223,13 +223,14 @@ To deactivate the printing of projections, use
 \label{Mult-match}}
 
 The basic version of \verb+match+ allows pattern-matching on simple
-patterns. As an extension, multiple and nested patterns are
-allowed, as in ML-like languages.
+patterns. As an extension, multiple nested patterns or disjunction of
+patterns are allowed, as in ML-like languages.
 
 The extension just acts as a macro that is expanded during parsing
 into a sequence of {\tt match} on simple patterns. Especially, a
-construction defined using the extended {\tt match} is printed under
-its expanded form.
+construction defined using the extended {\tt match} is generally
+printed under its expanded form (see~\texttt{Set Printing Matching} in
+section~\ref{SetPrintingMatching}).
 
 \SeeAlso chapter \ref{Mult-match-full}.
 
@@ -330,11 +331,40 @@ The general equivalence for an inductive type with one constructors {\tt C} is
 $\equiv$~
 {\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end}
 
-\subsection{Options for pretty-printing of {\tt match}
+\subsection{Controlling pretty-printing of {\tt match} expressions
 \label{printing-options}}
 
-There are three options controlling the pretty-printing of {\tt match}
-expressions.
+The following commands give some control over the pretty-printing of
+{\tt match} expressions.
+
+\subsubsection{Printing nested patterns
+\label{SetPrintingMatching}
+\comindex{Set Printing Matching}
+\comindex{Unset Printing Matching}
+\comindex{Test Printing Matching}}
+
+The Calculus of Inductive Constructions knows pattern-matching only
+over simple patterns. It is however convenient to re-factorize nested
+pattern-matching into a single pattern-matching over a nested pattern.
+{\Coq}'s printer try to do such limited re-factorization.
+
+\begin{quote}
+{\tt Set Printing Matching.}
+\end{quote}
+This tells {\Coq} to try to use nested patterns. This is the default
+behavior.
+
+\begin{quote}
+{\tt Unset Printing Matching.}
+\end{quote}
+This tells {\Coq} to print only simple pattern-matching problems in
+the same way as the {\Coq} kernel handles them.
+
+\begin{quote}
+{\tt Test Printing Matching.}
+\end{quote}
+This tells if the printing matching mode is on or off. The default is
+on.
 
 \subsubsection{Printing of wildcard pattern
 \comindex{Set Printing Wildcard}
@@ -1088,6 +1118,18 @@ the declaration
 \SeeAlso more examples in user contribution \texttt{category}
 (\texttt{Rocq/ALGEBRA}).
 
+\subsubsection{Print Canonical Projections.
+\comindex{Print Canonical Projections}}
+
+This displays the list of global names that are components of some
+canonical structure. For each of them, the canonical structure of
+which it is a projection is indicated. For instance, the above example 
+gives the following output:
+
+\begin{coq_example}
+Print Canonical Projections.
+\end{coq_example}
+
 \subsection{Implicit types of variables}
 
 It is possible to bind variable names to a given type (e.g. in a
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 2214864a..e7b825d7 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -64,15 +64,24 @@ That is, they are recognized by the following lexical class:
 \begin{center}
 \begin{tabular}{rcl} 
 {\firstletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt \_}
-% $\mid$ {\tt unicode-letter}  
+$\mid$ {\tt unicode-letter}  
 \\
 {\subsequentletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt 0..9}
 $\mid$ {\tt \_} % $\mid$ {\tt \$}
-$\mid$ {\tt '} \\
+$\mid$ {\tt '} 
+$\mid$ {\tt unicode-letter}  
+$\mid$ {\tt unicode-id-part} \\
 {\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{}
 \end{tabular}
 \end{center}
-All characters are meaningful. In particular, identifiers are case-sensitive.
+All characters are meaningful. In particular, identifiers are
+case-sensitive.  The entry {\tt unicode-letter} non-exhaustively
+includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian,
+Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical
+letter-like symbols, hyphens, non-breaking space, {\ldots} The entry
+{\tt unicode-id-part} non-exhaustively includes symbols for prime
+letters and subscripts.
+
 Access identifiers, written {\accessident}, are identifiers prefixed
 by \verb!.! (dot) without blank. They are used in the syntax of qualified
 identifiers.
@@ -308,7 +317,9 @@ chapter \ref{Addoc-syntax}.
 &&\\
 {\returntype} & ::= & {\tt return} {\term} \\
 &&\\
-{\eqn} & ::= & \nelist{\pattern}{\tt ,} {\tt =>} {\term}\\
+{\eqn} & ::= & \nelist{\multpattern}{\tt |} {\tt =>} {\term}\\
+&&\\
+{\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\
 &&\\
 {\pattern} & ::= & {\qualid} \nelist{\pattern}{}  \\
  & $|$ & {\pattern} {\tt as} {\ident}             \\
@@ -316,7 +327,9 @@ chapter \ref{Addoc-syntax}.
  & $|$ & {\qualid}                              \\
  & $|$ & {\tt \_}                                  \\
  & $|$ & {\num}                                 \\
- & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )}     
+ & $|$ & {\tt (} \nelist{\orpattern}{,} {\tt )}     \\
+\\
+{\orpattern} & ::= & \nelist{\pattern}{\tt |}\\
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of terms (continued)}
@@ -515,10 +528,11 @@ 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
+inductive type $I$). 
+The terms {\term$_1$}\ldots{\term$_n$} are called branches. In
 a simple pattern \qualid~\nelist{\ident}{}, the qualified identifier
 {\qualid} is intended to
-be a constructor. There should be a branch for every constructor of
+be a constructor. There should be one branch for every constructor of
 $I$.
 
 The {\returntype} is used to compute the resulting type of the whole
@@ -530,9 +544,8 @@ 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 / then / else} and
-{\tt let (}\ldots{\tt ) :=} \ldots {\tt in}\ldots. \SeeAlso
-section~\ref{Mult-match} for details and examples.
+two constructors: {\tt if {\ldots} then {\ldots} else {\ldots}} and
+{\tt let (}\nelist{\ldots}{,}{\tt ) :=} {\ldots} {\tt in} {\ldots}.
 
 \SeeAlso Section~\ref{Mult-match} for details and examples.
 
@@ -761,12 +774,17 @@ environment, provided that {\term} is well-typed.
        {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,%
        {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
        {\tt .}
+
+\item {\tt Example {\ident} := {\term}.}\\
+{\tt Example {\ident} {\tt :}{\term$_1$} := {\term$_2$}.}\\
+{\tt Example {\ident} {\binder$_1$}\ldots{\binder$_n$}
+       {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
+\comindex{Example}
+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}
@@ -1062,17 +1080,23 @@ inductive types The extended syntax is:
 
 \medskip
 {\tt 
-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$}  \\
+\begin{tabular}{l}
+Inductive {\ident$_1$} {\params} : {\type$_1$} :=  \\
+\begin{tabular}{clcl}
+   & {\ident$_1^1$}     &:& {\type$_1^1$} \\
+ | & {\ldots} && \\
+ | & {\ident$_{n_1}^1$} &:& {\type$_{n_1}^1$}
+\end{tabular}  \\
 with\\
-\mbox{}\hspace{0.1cm} .. \\
+~{\ldots} \\
 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$}.
-}}
+\begin{tabular}{clcl}
+   & {\ident$_1^m$}     &:& {\type$_1^m$} \\
+ | & {\ldots} \\
+ | & {\ident$_{n_m}^m$} &:& {\type$_{n_m}^m$}.
+\end{tabular}
+\end{tabular}
+}
 \medskip
 
 \Example
@@ -1184,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
@@ -1205,8 +1231,8 @@ 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 :
+fixpoints where only one argument has an inductive type. For instance,
+one can define the addition function as :
 
 \begin{coq_example}
 Fixpoint add (n m:nat) {struct n} : nat :=
@@ -1323,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.
 
@@ -1416,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
@@ -1508,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 :=
@@ -1606,9 +1626,13 @@ After a statement, {\Coq} needs a proof.
 
 \begin{Variants} 
 \item {\tt Lemma {\ident} : {\type}.}\\ 
-It is a synonymous of \texttt{Theorem}
-\item {\tt Remark {\ident} : {\type}.}\\ 
-It is a synonymous of \texttt{Theorem}
+      {\tt Remark {\ident} : {\type}.}\\ 
+      {\tt Fact {\ident} : {\type}.}\\ 
+      {\tt Corollary {\ident} : {\type}.}\\ 
+      {\tt Proposition {\ident} : {\type}.}\\ 
+\comindex{Proposition}
+\comindex{Corollary}
+All these commands are synonymous of \texttt{Theorem}
 % Same as {\tt Theorem} except
 % that if this statement is in one or more levels of sections then the
 % name {\ident} will be accessible only prefixed by the sections names
@@ -1616,8 +1640,6 @@ 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}.}\\ 
-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}.} \\
@@ -1684,4 +1706,4 @@ To be able to unfold a proof, you should end the proof by {\tt Defined}
 % TeX-master: "Reference-Manual"
 % End: 
 
-% $Id: RefMan-gal.tex 8915 2006-06-07 15:17:13Z courtieu $ 
+% $Id: RefMan-gal.tex 9040 2006-07-11 18:06:49Z notin $ 
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index 3c73c141..104338ea 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -11,9 +11,10 @@ them respectively. % CREDITS ? Proof general, lablgtk, ...
 \CoqIDE{} is run by typing the command \verb|coqide| on the command
 line. Without argument, the main screen is displayed with an ``unnamed
 buffer'', and with a file name as argument, another buffer displaying
-the contents of that file. Additionally, coqide accepts the same
-options as coqtop, given in Chapter~\ref{Addoc-coqc}, the ones having
-obviously no meaning for \CoqIDE{} being ignored.
+the contents of that file. Additionally, \verb|coqide| accepts the same
+options as \verb|coqtop|, given in Chapter~\ref{Addoc-coqc}, the ones having
+obviously no meaning for \CoqIDE{} being ignored. Additionally, \verb|coqide| accepts the option \verb|-enable-geoproof| to enable the support for \emph{GeoProof} \footnote{\emph{GeoProof} is dynamic geometry software which can be used in conjunction with \CoqIDE{} to interactively build a Coq statement corresponding to a geometric figure. More information about \emph{GeoProof} can be found here: \url{http://home.gna.org/geoproof/} }. 
+  
 
 \begin{figure}[t]
 \begin{center}
@@ -319,7 +320,7 @@ or
 
     
 
-% $Id: RefMan-ide.tex 8626 2006-03-14 15:01:00Z notin $ 
+% $Id: RefMan-ide.tex 8945 2006-06-10 12:04:14Z jnarboux $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index de9897c4..e7400232 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -103,16 +103,23 @@ is understood as
 {\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
 & | &
 {\tt match} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\
+& | &
+{\tt lazymatch goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
+& | &
+{\tt lazymatch reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
+& | &
+{\tt lazymatch} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\
 & | & {\tt abstract} {\atom}\\
 & | & {\tt abstract} {\atom} {\tt using} {\ident} \\
 & | & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
 & | & {\tt solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
-& | & {\tt idtac} ~|~ {\tt idtac} {\qstring}\\
-& | & {\tt fail} ~|~ {\tt fail} {\naturalnumber} {\qstring}\\
+& | & {\tt idtac} \sequence{\messagetoken}{}\\
+& | & {\tt fail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\
 & | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\
 & | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\
 & | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
 & | & {\tt type of} {\term}\\
+& | & {\tt external} {\qstring} {\qstring} \nelist{\tacarg}{}\\
 & | & {\tt constr :} {\term}\\
 & | & \atomictac\\
 & | & {\qualid} \nelist{\tacarg}{}\\
@@ -122,6 +129,8 @@ is understood as
            {\qualid} \\
 & | & ()\\
 & | & {\tt (} {\tacexpr} {\tt )}\\
+\\
+{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\term} ~|~ {\integer} \\
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of the tactic language}
@@ -266,6 +275,12 @@ 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
 $v_0$ does not generate exactly $n$ subgoals.
 
+\variant If no tactic is given for the $i$-th generated subgoal, it
+behaves as if the tactic {\tt idtac} were given. For instance, {\tt
+split ; [ | auto ]} is a shortcut for
+{\tt split ; [ idtac | auto ]}.
+
+
 \subsubsection{For loop}
 \tacindex{do}
 \index{Tacticals!do@{\tt do}}
@@ -369,10 +384,13 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic.
 
 The constant {\tt idtac} is the identity tactic: it leaves any goal
 unchanged but it appears in the proof script.
-\begin{quote}
-{\tt idtac} and {\tt idtac "message"}
-\end{quote}
-The latter variant prints the string on the standard output.
+
+\variant {\tt idtac \nelist{\messagetoken}{}}
+
+This prints the given tokens. Strings and integers are printed
+literally. If a term is given, it is printed, its variables being
+interpreted in the current environment. In particular, if a variable
+is given, its value is printed.
 
 
 \subsubsection{Failing}
@@ -381,17 +399,24 @@ 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:
-\begin{quote}
-{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"}
-\end{quote}
+catched by {\tt try} or {\tt match goal}. 
+
+\begin{Variants}
+\item {\tt fail $n$}\\
 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
 (backtracking). If non zero, the current {\tt match goal} block or
 {\tt try} command is aborted and the level is decremented.
 
-\ErrMsg \errindex{Tactic Failure "message" (level $n$)}.
+\item {\tt fail \nelist{\messagetoken}{}}\\
+The given tokens are used for printing the failure message.
+
+\item {\tt fail $n$ \nelist{\messagetoken}{}}\\
+This is a combination of the previous variants.
+\end{Variants}
+
+\ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}.
 
 \subsubsection{Local definitions}
 \index{Ltac!let}
@@ -464,10 +489,13 @@ The {\tacexpr} is evaluated and should yield a term which is matched
 pattern matching instantiations to the metavariables. If the matching
 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
-goal}). If all clauses fail (in particular, there is no pattern {\_})
-then a no-matching error is raised.
+any. If {\tacexpr}$_1$ evaluates to a tactic and the {\tt match}
+expression is in position to be applied to a goal (e.g. it is not
+bound to a variable by a {\tt let in}, then this tactic is applied. If
+the tactic succeeds, the list of resulting subgoals is the result of
+the {\tt match} expression. On the opposite, if it fails, the next
+pattern is tried. If all clauses fail (in particular, there is no
+pattern {\_}) then a no-matching error is raised.
 
 \begin{ErrMsgs}
 
@@ -481,7 +509,8 @@ then a no-matching error is raised.
 
 \end{ErrMsgs}
 
-\index{context!in pattern}
+\begin{Variants}
+\item \index{context!in pattern}
 There is a special form of patterns to match a subterm against the
 pattern:
 \begin{quote}
@@ -493,11 +522,36 @@ is the initial term where the matched subterm is replaced by a
 hole. The definition of {\tt context} in expressions below will show
 how to use such term contexts.
 
-This operator never makes backtracking. If there are several subterms
-matching the pattern, only the first match is considered. Note that
-the order of matching is left unspecified.
-%% TODO: clarify this point! It *should* be specified
+If the evaluation of the right-hand-side of a valid match fails, the
+next matching subterm is tried. If no further subterm matches, the
+next clause is tried. Matching subterms are considered top-bottom and
+from left to right (with respect to the raw printing obtained by
+setting option {\tt Printing All}, see section~\ref{SetPrintingAll}).
+
+\begin{coq_example}
+Ltac f x :=
+  match x with
+    context f [S ?X] => 
+    idtac X;                    (* To display the evaluation order *)
+    assert (p := refl_equal 1 : X=1);    (* To filter the case X=1 *)
+    let x:= context f[O] in assert (x=O) (* To observe the context *)
+  end.
+Goal True.
+f (3+4).
+\end{coq_example}
+
+\item \index{lazymatch!in Ltac}
+\index{Ltac!lazymatch}
+Using {\tt lazymatch} instead of {\tt match} has an effect if the
+right-hand-side of a clause returns a tactic. With {\tt match}, the
+tactic is applied to the current goal (and the next clause is tried if
+it fails). With {\tt lazymatch}, the tactic is directly returned as
+the result of the whole {\tt lazymatch} block without being first
+tried to be applied to the goal. Typically, if the {\tt lazymatch}
+block is bound to some variable $x$ in a {\tt let in}, then tactic
+expression gets bound to the variable $x$.
 
+\end{Variants}
 
 \subsubsection{Pattern matching on goals}
 \index{Ltac!match goal}
@@ -521,8 +575,6 @@ We can make pattern matching on goals using the following expression:
 \end{tabbing}
 \end{quote}
 
-% TODO: specify order of hypothesis and explain reverse...
-
 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 {\cpattern}$_1$ is matched by the conclusion of the
@@ -535,7 +587,9 @@ 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. Note also that matching against subterms (using the {\tt
+context} {\ident} {\tt [} {\cpattern} {\tt ]}) is available and may
+itself induce extra backtrackings.
 
 \ErrMsg \errindex{No matching clauses for match goal}
 
@@ -552,6 +606,36 @@ pattern, the goal hypothesis are matched in order (fresher hypothesis
 first), but it possible to reverse this order (older first) with
 the {\tt match reverse goal with} variant.
 
+\variant
+\index{lazymatch goal!in Ltac}
+\index{Ltac!lazymatch goal}
+\index{lazymatch reverse goal!in Ltac}
+\index{Ltac!lazymatch reverse goal}
+Using {\tt lazymatch} instead of {\tt match} has an effect if the
+right-hand-side of a clause returns a tactic. With {\tt match}, the
+tactic is applied to the current goal (and the next clause is tried if
+it fails). With {\tt lazymatch}, the tactic is directly returned as
+the result of the whole {\tt lazymatch} block without being first
+tried to be applied to the goal. Typically, if the {\tt lazymatch}
+block is bound to some variable $x$ in a {\tt let in}, then tactic
+expression gets bound to the variable $x$.
+
+\begin{coq_example}
+Ltac test_lazy :=
+  lazymatch goal with
+  | _ => idtac "here"; fail 
+  | _ => idtac "wasn't lazy"; trivial
+  end.
+Ltac test_eager :=
+  match goal with
+  | _ => idtac "here"; fail 
+  | _ => idtac "wasn't lazy"; trivial
+  end.
+Goal True.
+test_lazy || idtac "was lazy".
+test_eager || idtac "was lazy".
+\end{coq_example}
+
 \subsubsection{Filling a term context}
 \index{context!in expression}
 
@@ -585,13 +669,6 @@ 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{{\tt type of} {\term}}
-%\tacindex{type of}
-\index{Ltac!type of}
-\index{type of!in Ltac}
-
-This tactic computes the type of {\term}.
-
 \subsubsection{Computing in a constr}
 \index{Ltac!eval}
 \index{eval!in Ltac}
@@ -604,6 +681,16 @@ 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}.
 
+\subsubsection{Type-checking a term}
+%\tacindex{type of}
+\index{Ltac!type of}
+\index{type of!in Ltac}
+
+The following returns the type of {\term}:
+
+\begin{quote}
+{\tt type of} {\term}
+\end{quote}
 
 \subsubsection{Accessing tactic decomposition}
 \tacindex{info}
@@ -635,10 +722,76 @@ without having to cut manually the proof in smaller lemmas.
 
 \ErrMsg \errindex{Proof is not complete}
 
+\subsubsection{Calling an external tactic}
+\index{Ltac!external}
+
+The tactic {\tt external} allows to run an executable outside the
+{\Coq} executable. The communication is done via an XML encoding of
+constructions. The syntax of the command is
+
+\begin{quote}
+{\tt external} "\textsl{command}" "\textsl{request}" \nelist{\tacarg}{}
+\end{quote}
+
+The string \textsl{command}, to be interpreted in the default
+execution path of the operating system, is the name of the external
+command. The string \textsl{request} is the name of a request to be
+sent to the external command. Finally the list of tactic arguments
+have to evaluate to terms. An XML tree of the following form is sent
+to the standard input of the external command.
+\medskip
+
+\begin{tabular}{l}
+\texttt{<REQUEST req="}\textsl{request}\texttt{">}\\
+the XML tree of the first argument\\
+{\ldots}\\
+the XML tree of the last argument\\
+\texttt{</REQUEST>}\\
+\end{tabular}
+\medskip
+
+Conversely, the external command must send on its standard output an
+XML tree of the following forms:
+
+\medskip
+\begin{tabular}{l}
+\texttt{<TERM>}\\
+the XML tree of a term\\
+\texttt{</TERM>}\\
+\end{tabular}
+\medskip
+
+\noindent or 
+
+\medskip
+\begin{tabular}{l}
+\texttt{<CALL uri="}\textsl{ltac\_qualified\_ident}\texttt{">}\\
+the XML tree of a first argument\\
+{\ldots}\\
+the XML tree of a last argument\\
+\texttt{</CALL>}\\
+\end{tabular}
+
+\medskip
+\noindent where \textsl{ltac\_qualified\_ident} is the name of a
+defined {\ltac} function and each subsequent XML tree is recursively a
+\texttt{CALL} or a \texttt{TERM} node.
+
+The Document Type Definition (DTD) for terms of the Calculus of
+Inductive Constructions is the one developed as part of the MoWGLI
+European project. It can be found in the file {\tt dev/doc/cic.dtd} of
+the {\Coq} source archive.
+
+An example of parser for this DTD, written in the Objective Caml -
+Camlp4 language, can be found in the file {\tt parsing/g\_xml.ml4} of
+the {\Coq} source archive.
+
 \section{Tactic toplevel definitions}
 \comindex{Ltac}
 
-Basically, tactics toplevel definitions are made as follows:
+\subsection{Defining {\ltac} functions}
+
+Basically, {\ltac} 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
@@ -649,8 +802,8 @@ Basically, tactics toplevel definitions are made as follows:
 {\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=}
 {\tacexpr}
 \end{quote}
-This defines a new tactic that can be used in any tactic script or new
-tactic toplevel definition.
+This defines a new {\ltac} function that can be used in any tactic
+script or new {\ltac} toplevel definition.
 
 \Rem The preceding definition can equivalently be written:
 \begin{quote}
@@ -674,8 +827,49 @@ possible with the syntax:
 %usual except that the substitutions are lazily carried out (when an identifier
 %to be evaluated is the name of a recursive definition).
 
-\endinput
 
+\subsection{Printing {\ltac} tactics}
+\comindex{Print Ltac}
+
+Defined {\ltac} functions can be displayed using the command
+
+\begin{quote}
+{\tt Print Ltac {\qualid}.}
+\end{quote}
+
+\section{Debugging {\ltac} tactics}
+\comindex{Set Ltac Debug}
+\comindex{Unset Ltac Debug}
+\comindex{Test Ltac Debug}
+
+The {\ltac} interpreter comes with a step-by-step debugger. The
+debugger can be activated using the command
+
+\begin{quote}
+{\tt Set Ltac Debug.}
+\end{quote}
+
+\noindent and deactivated using the command
+
+\begin{quote}
+{\tt Unset Ltac Debug.}
+\end{quote}
+
+To know if the debugger is on, use the command \texttt{Test Ltac Debug}.
+When the debugger is activated, it stops at every step of the
+evaluation of the current {\ltac} expression and it prints information
+on what it is doing. The debugger stops, prompting for a command which
+can be one of the following:
+
+\medskip
+\begin{tabular}{ll}
+simple newline: & go to the next step\\
+h: & get help\\
+x: & exit current evaluation\\
+s: & continue current evaluation without stopping\\
+r$n$: & advance $n$ steps further\\
+\end{tabular}
+\endinput
 
 \subsection{Permutation on closed lists}
 
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 9f6f2abc..44a88034 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -55,6 +55,11 @@ This command is used to start an interactive module named {\ident}.
   {\modbindings}. The output module type is verified against the
   module type {\modtype}.
 
+\item\texttt{Module [Import|Export]}
+
+  Behaves like \texttt{Module}, but automatically imports or exports
+  the module.
+
 \end{Variants}
 
 \subsection{\tt End {\ident}
@@ -139,38 +144,9 @@ Defines a module type {\ident} equal to {\modtype}.
   {\modbindings} and returning {\modtype}.
 \end{Variants}
 
-\subsection{\tt Declare Module {\ident}}
-
-Starts an interactive module declaration. This command is available
-only in module types. 
-
-\begin{Variants}
-
-\item{\tt Declare Module {\ident} {\modbindings}}
-
-  Starts an interactive declaration of a functor with parameters given
-  by {\modbindings}.
-
-% Particular case of the next item
-%\item{\tt Declare Module {\ident} \verb.<:. {\modtype}}
-%
-%  Starts an interactive declaration of a module satisfying {\modtype}.
-
-\item{\tt Declare Module {\ident} {\modbindings} \verb.<:. {\modtype}}
-
-  Starts an interactive declaration of a functor with parameters given
-  by {\modbindings} (possibly none). The declared output module type is
-  verified against the module type {\modtype}.
-
-\end{Variants}
-
-\subsection{\tt End {\ident}}
-
-This command closes the interactive declaration of module {\ident}.
-
 \subsection{\tt Declare Module {\ident} : {\modtype}}
 
-Declares a module of {\ident} of type {\modtype}. This command is available
+Declares a module {\ident} of type {\modtype}. This command is available
 only in module types. 
 
 \begin{Variants}
@@ -189,6 +165,11 @@ only in module types.
   Declares a module equal to the module {\qualid}, verifying that the
   module type of the latter is a subtype of {\modtype}.
 
+\item\texttt{Declare Module [Import|Export] {\ident} := {\qualid}}
+
+  Declares a modules {\ident} of type {\modtype}, and imports or
+  exports it directly.
+
 \end{Variants}
 
 
@@ -389,6 +370,11 @@ Prints the module type and (optionally) the body of the module {\ident}.
 
 Prints the module type corresponding to {\ident}.
 
+\subsection{\texttt{Locate Module {\qualid}}
+\comindex{Locate Module}}
+
+Prints the full name of the module {\qualid}.
+
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index e92cde74..1d2057a9 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -334,6 +334,72 @@ Locate I.Dont.Exist.
 
 \SeeAlso Section \ref{LocateSymbol}
 
+\subsection{The {\sc Whelp} searching tool
+\label{Whelp}}
+
+{\sc Whelp} is an experimental searching and browsing tool for the
+whole {\Coq} library and the whole set of {\Coq} user contributions.
+{\sc Whelp} requires a browser to work. {\sc Whelp} has been developed
+at the University of Bologna as part of the HELM\footnote{Hypertextual
+Electronic Library of Mathematics} and MoWGLI\footnote{Mathematics on
+the Web, Get it by Logics and Interfaces} projects.  It can be invoked
+directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a
+graphical environment is also running. The browser to use can be
+selected by setting the environment variable {\tt
+COQREMOTEBROWSER}. If not explicitly set, it defaults to
+\verb!netscape -remote "OpenURL(%s)"!  or
+\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the
+underlying operating system (in the command, the string \verb!%s!
+serves as metavariable for the url to open).
+
+The {\sc Whelp} commands are:
+
+\subsubsection{\tt Whelp Locate "{\sl reg\_expr}".
+\comindex{Whelp Locate}}
+
+This command opens a browser window and displays the result of seeking
+for all names that match the regular expression {\sl reg\_expr} in the
+{\Coq} library and user contributions. The regular expression can
+contain the special operators are * and ? that respectively stand for
+an arbitrary substring and for exactly one character.
+
+\variant {\tt Whelp Locate {\ident}.}\\
+This is equivalent to {\tt Whelp Locate "{\ident}"}.
+
+\subsubsection{\tt Whelp Match {\pattern}.
+\comindex{Whelp Match}}
+
+This command opens a browser window and displays the result of seeking
+for all statements that match the pattern {\pattern}. Holes in the
+pattern are represented by the wildcard character ``\_''.
+
+\subsubsection{\tt Whelp Instance {\pattern}.}
+\comindex{Whelp Instance}
+
+This command opens a browser window and displays the result of seeking
+for all statements that are instances of the pattern {\pattern}. The
+pattern is here assumed to be an universally quantified expression.
+
+\subsubsection{\tt Whelp Elim {\qualid}.}
+\comindex{Whelp Elim}
+
+This command opens a browser window and displays the result of seeking
+for all statements that have the ``form'' of an elimination scheme
+over the type denoted by {\qualid}.
+
+\subsubsection{\tt Whelp Hint {\term}.}
+\comindex{Whelp Hint}
+
+This command opens a browser window and displays the result of seeking
+for all statements that can be instantiated so that to prove the
+statement {\term}.
+
+\variant {\tt Whelp Hint.}\\ This is equivalent to {\tt Whelp Hint
+{\sl goal}} where {\sl goal} is the current goal to prove. Notice that
+{\Coq} does not send the local environment of definitions to the {\sc
+Whelp} tool so that it only works on requests strictly based on, only,
+definitions of the standard library and user contributions.
+
 \section{Loading files}
 
 \Coq\ offers the possibility of loading different
@@ -765,7 +831,39 @@ This command displays the current nesting depth used for display.
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
-% $Id: RefMan-oth.tex 8606 2006-02-23 13:58:10Z herbelin $ 
+\section{Controlling the conversion algorithm}
+
+{\Coq} comes with two algorithms to check the convertibility of types
+(see section~\ref{convertibility}). The first algorithm lazily
+compares applicative terms while the other is a brute-force but efficient
+algorithm that first normalizes the terms before comparing them.  The
+second algorithm is based on a bytecode representation of terms
+similar to the bytecode representation used in the ZINC virtual
+machine~\cite{Leroy90}. It is specially useful for intensive
+computation of algebraic values, such as numbers, and for reflexion-based
+tactics.
+
+\subsection{\tt Set Virtual Machine
+\label{SetVirtualMachine}
+\comindex{Set Virtual Machine}}
+
+This activates the bytecode-based conversion algorithm.
+
+\subsection{\tt Unset Virtual Machine
+\comindex{Unset Virtual Machine}}
+
+This deactivates the bytecode-based conversion algorithm.
+
+\subsection{\tt Test Virtual Machine
+\comindex{Test Virtual Machine}}
+
+This tells if the bytecode-based conversion algorithm is
+activated. The default behavior is to have the bytecode-based
+conversion algorithm deactivated.
+
+\SeeAlso sections~\ref{vmcompute} and~\ref{vmoption}.
+
+% $Id: RefMan-oth.tex 9044 2006-07-12 13:22:17Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 2f79e5f0..43216ed0 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -556,19 +556,19 @@ unresolved implicit has been implemented by Hugo Herbelin.
 Laurent Théry's contribution on strings and Pierre Letouzey and
 Jean-Christophe Filliâtre's contribution on finite maps have been
 integrated to the {\Coq} standard library. Pierre Letouzey developed a
-library about finite sets ``à la Objective Caml'' and extended the
-lists library. Pierre Letouzey's contribution on rational numbers
-has been integrated too.
+library about finite sets ``à la Objective Caml''. With Jean-Marc
+Notin, he extended the library on lists. Pierre Letouzey's
+contribution on rational numbers has been integrated and extended..
 
 Pierre Corbineau extended his tactic for solving first-order
-statements. He wrote a reflexion-based intuitionistic tautology
+statements. He wrote a reflection-based intuitionistic tautology
 solver.
 
-Jean-Marc Notin took care of {\textsf{coqdoc}} and of the general
-maintenance of the system.
+Jean-Marc Notin significantly contributed to the general maintenance
+of the system. He also took care of {\textsf{coqdoc}}.
 
 \begin{flushright}
-Palaiseau, Apr. 2006\\
+Palaiseau, July 2006\\
 Hugo Herbelin
 \end{flushright}
 
@@ -577,7 +577,7 @@ Hugo Herbelin
 % Integration of ZArith lemmas from Sophia and Nijmegen.
 
 
-% $Id: RefMan-pre.tex 8941 2006-06-09 16:43:42Z herbelin $ 
+% $Id: RefMan-pre.tex 9030 2006-07-07 15:37:23Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 739ca6b5..8c1a7824 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -163,28 +163,21 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels:
   current section.
 \end{Variants}
 
-\subsection{\tt Proof {\term}.}\comindex{Proof}
+\subsection{\tt Proof {\term}.}
+\comindex{Proof}
+\label{BeginProof}
 This command applies in proof editing mode. It is equivalent to {\tt
   exact {\term}; Save.} That is, you have to give the full proof in
 one gulp, as a proof term (see section \ref{exact}).
 
-\begin{Variants}
-
-\item{\tt Proof.}
+\variant {\tt Proof.}
   
   Is a noop which is useful to delimit the sequence of tactic commands
   which start a proof, after a {\tt Theorem} command.  It is a good
   practice to use {\tt Proof.} as an opening parenthesis, closed in
   the script with a closing {\tt Qed.}
 
-\item{\tt Proof with {\tac}.}
-  
-  This command may be used to start a proof. It defines a default
-  tactic to be used each time a tactic command is ended by
-  ``\verb#...#''. In this case the tactic command typed by the user is
-  equivalent to \emph{command};{\tac}.
-
-\end{Variants}
+\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}.
 
 \subsection{\tt Abort.}
 \comindex{Abort}
@@ -381,7 +374,7 @@ All the hypotheses remains usable in the proof development.
 This command goes back to the default mode which is to print all
 available hypotheses.
 
-% $Id: RefMan-pro.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $
+% $Id: RefMan-pro.tex 9030 2006-07-07 15:37:23Z herbelin $
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 341e766e..e41983dc 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -221,6 +221,14 @@ The command to display the current state of the {\Coq} term parser is
 \tt Print Grammar constr.
 \end{quote}
 
+\variant
+
+\comindex{Print Grammar pattern}
+{\tt Print Grammar pattern.}\\
+
+This displays the state of the subparser of patterns (the parser
+used in the grammar of the {\tt match} {\tt with} constructions).
+
 \subsection{Displaying symbolic notations}
 
 The command \texttt{Notation} has an effect both on the {\Coq} parser and
@@ -436,9 +444,10 @@ Locate "'exists' _ , _".
 \SeeAlso Section \ref{Locate}.
 
 \begin{figure}
+\begin{small}
 \begin{centerframe}
 \begin{tabular}{lcl}
-{\sentence} & ::= &
+{\sentence} & ::= & 
    \texttt{Notation} \zeroone{\tt Local} {\str} \texttt{:=} {\term} 
    \zeroone{\modifiers} \zeroone{:{\scope}} .\\
   & $|$ & 
@@ -474,6 +483,7 @@ Locate "'exists' _ , _".
   & $|$ & {\tt format} {\str} 
 \end{tabular}
 \end{centerframe}
+\end{small}
 \caption{Syntax of the variants of {\tt Notation}}
 \label{notation-syntax}
 \end{figure}
@@ -633,7 +643,8 @@ instance the infix symbol \verb=+= can be used to denote distinct
 definitions of an additive operator. Depending on which interpretation
 scopes is currently open, the interpretation is different.
 Interpretation scopes can include an interpretation for
-numerals. However, this is only made possible at the {\ocaml} level.
+numerals and strings. However, this is only made possible at the
+{\ocaml} level.
 
 See Figure \ref{notation-syntax} for the syntax of notations including
 the possibility to declare them in a given scope.  Here is a typical
@@ -824,6 +835,21 @@ type {\tt positive} (binary strictly positive numbers). It is
 delimited by key {\tt positive} and comes with an interpretation for
 numerals as closed term of type {\tt positive}.
 
+\subsubsection{\tt Q\_scope}
+
+This includes the standard arithmetical operators and relations on
+type {\tt Q} (rational numbers defined as fractions of an integer and
+a strictly positive integer modulo the equality of the
+numerator-denominator cross-product). As for numerals, only $0$ and
+$1$ have an interpretation in scope {\tt Q\_scope} (their
+interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively).
+
+\subsubsection{\tt Qc\_scope}
+
+This includes the standard arithmetical operators and relations on the
+type {\tt Qc} of rational numbers defined as the type of irreducible
+fractions of an integer and a strictly positive integer.
+
 \subsubsection{\tt real\_scope}
 
 This includes the standard arithmetical operators and relations on
@@ -853,6 +879,25 @@ delimited by key {\tt list}.
 
 This includes the notation for pairs. It is delimited by key {\tt core}.
 
+\subsubsection{\tt string\_scope}
+
+This includes notation for strings as elements of the type {\tt
+string}.  Special characters and escaping follow {\Coq} conventions
+on strings (see page~\pageref{strings}). Especially, there is no
+convention to visualize non printable characters of a string.  The
+file {\tt String.v} shows an example that contains quotes, a newline
+and a beep (i.e. the ascii character of code 7).
+
+\subsubsection{\tt char\_scope}
+
+This includes interpretation for all strings of the form
+\verb!"!$c$\verb!"! where $c$ is an ascii character, or of the form
+\verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly
+with leading 0's), or of the form \verb!""""!. Their respective
+denotations are the ascii code of $c$, the decimal ascii code $nnn$,
+or the ascii code of the character \verb!"! (i.e. the ascii code
+34), all of them being represented in the type {\tt ascii}.
+
 \subsection{Displaying informations about scopes}
 
 \subsubsection{\tt Print Visibility}
@@ -948,11 +993,14 @@ tactic language\footnote{Tactic notations are just a simplification of
 the {\tt Grammar tactic simple\_tactic} command that existed in
 versions prior to version 8.0.}. Tactic notations obey the following
 syntax
+\medskip
 
+\noindent
 \begin{tabular}{lcl}
-{\sentence} & ::= & \texttt{Tactic Notation} {\str} \sequence{\proditem}{} \\
+{\sentence} & ::= & \texttt{Tactic Notation} {\taclevel} \sequence{\proditem}{} \\
 & & \texttt{:= {\tac} .}\\
 {\proditem} & ::= & {\str} $|$ {\tacargtype}{\tt ({\ident})} \\ 
+{\taclevel} & ::= & $|$ {\tt (at level} {\naturalnumber}{\tt )} \\
 {\tacargtype} & ::= &
 %{\tt preident} $|$
 {\tt ident} $|$
@@ -966,14 +1014,18 @@ syntax
 {\tt int\_or\_var} $|$
 {\tt tactic} $|$
 \end{tabular}
+\medskip
 
-A tactic notation {\tt Tactic Notation {\str} {\sequence{\proditem}{}}
-:= {\tac}} extends the parser and pretty-printer of tactics with a
-new rule made of the juxtaposition of the head name of the tactic
-{\str} and the list of its production items (in the syntax of
-production items, {\str} stands for a terminal symbol and {\tt
-\tacargtype({\ident}) for non terminal entries}. It then evaluates
-into the tactic expression {\tac}.
+A tactic notation {\tt Tactic Notation {\taclevel}
+{\sequence{\proditem}{}} := {\tac}} extends the parser and
+pretty-printer of tactics with a new rule made of the list of
+production items. It then evaluates into the tactic expression
+{\tac}. For simple tactics, it is recommended to use a terminal
+symbol, i.e. a {\str}, for the first production item.  The tactic
+level indicates the parsing precedence of the tactic notation. This
+information is particularly relevant for notations of tacticals.
+Levels 0 to 5 are available. To know the parsing precedences of the
+existing tacticals, use the command {\tt Print Grammar tactic.}
 
 Each type of tactic argument has a specific semantic regarding how it
 is parsed and how it is interpreted. The semantic is described in the
@@ -1008,7 +1060,7 @@ for {\tt integer}. This is the reason for introducing a special entry
 syntactically includes identifiers in order to be usable in tactic
 definitions.
 
-% $Id: RefMan-syn.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ 
+% $Id: RefMan-syn.tex 9012 2006-07-05 16:03:16Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f034df41..24699873 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -69,6 +69,13 @@ convertible (see Section~\ref{conv-rules}).
 \item \errindex{Not an exact proof}
 \end{ErrMsgs}
 
+\begin{Variants}
+  \item \texttt{eexact \term}\tacindex{eexact} 
+    
+    This tactic behaves like \texttt{exact} but is able to handle terms with meta-variables. 
+
+\end{Variants}
+
 
 \subsection{\tt refine \term
 \tacindex{refine}
@@ -112,6 +119,15 @@ subgoal is proved. Otherwise, it fails.
 \item  \errindex{No such assumption}
 \end{ErrMsgs}
 
+\begin{Variants}
+  \item \texttt{eassumption}
+
+    This tactic behaves like \texttt{assumption} but is able to handle
+    goals with meta-variables.
+
+\end{Variants}
+
+
 \subsection{\tt clear {\ident}
 \tacindex{clear}
 \label{clear}}
@@ -133,6 +149,10 @@ usable in the proof development.
   its body. Otherwise said, this tactic turns a definition into an
   assumption.
 
+\item \texttt{clear - {\ident}.} 
+
+  This tactic clears all hypotheses except the ones depending in {\ident}.
+
 \end{Variants}
 
 \begin{ErrMsgs}
@@ -506,6 +526,20 @@ in the list of subgoals remaining to prove.
   following subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U
     -> T} comes first in the list of remaining subgoal to prove.
 
+\item \texttt{assert {\form} by {\tac}}\tacindex{assert by}
+  
+  This tactic behaves like \texttt{assert} but tries to apply {\tac}
+  to any subgoals generated by \texttt{assert}.
+
+\item \texttt{assert {\form} as {\ident}\tacindex{assert as}}
+
+   This tactic behaves like \texttt{assert ({\ident} : {\form})}.
+
+\item \texttt{pose proof {\term} as {\ident}}
+
+  This tactic behaves like \texttt{assert ({\ident:T} by exact {\term}} where
+  \texttt{T} is the type of {\term}. 
+
 \end{Variants}
 
 % PAS CLAIR;
@@ -721,6 +755,7 @@ performs the conversion in hypotheses $H_1\ldots H_n$.
 \tacindex{cbv}
 \tacindex{lazy}
 \tacindex{compute}}
+\label{vmcompute}
 
 These parameterized reduction tactics apply to any goal and perform
 the normalization of the goal according to the specified flags. Since
@@ -764,6 +799,16 @@ computational expressions (i.e. with few dead code).
 \item {\tt compute} \tacindex{compute} 
   
   This tactic is an alias for {\tt cbv beta delta evar iota zeta}.
+
+\item {\tt vm\_compute} \tacindex{vm\_compute}
+
+  This tactic evaluates the goal using the optimized call-by-value
+  evaluation bytecode-based virtual machine. This algorithm is
+  dramatically more efficient than the algorithm used for the {\tt
+  cbv} tactic, but it cannot be fine-tuned. It is specially
+  interesting for full evaluation of algebraic objects. This includes
+  the case of reflexion-based tactics.
+
 \end{Variants}
 
 \begin{ErrMsgs}
@@ -1012,6 +1057,14 @@ equivalent to {\tt intros; apply ci}.
     these expressions are equivalent to the corresponding {\tt
     constructor $i$ with \bindinglist}.
 
+\item \texttt{econstructor}
+
+  This tactic behaves like \texttt{constructor} but is able to
+  introduce existential variables if an instanciation for a variable
+  cannot be found (cf \texttt{eapply}). The tactics \texttt{eexists},
+  \texttt{esplit}, \texttt{eleft} and \texttt{eright} follows the same
+  behaviour.
+
 \end{Variants}
 
 \section{Eliminations (Induction and Case Analysis)}
@@ -1096,6 +1149,11 @@ induction n.
 scheme of name {\qualid}. It does not expect that the type of
 {\term} is inductive.
 
+\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}}
+
+  where {\qualid} is an induction principle with complex predicates
+  (like the ones generated by function induction).
+
 \item {\tt induction {\term} using {\qualid} as {\intropattern}}
 
   This combines {\tt induction {\term} using {\qualid}}
@@ -1233,6 +1291,10 @@ last introduced hypothesis.
 {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
 {\tt [} $p_{1} $\ldots $p_{n}$ {\tt ]}.
 
+\item \texttt{pose proof {\term} as {\intropattern}}
+
+  This tactic behaves like \texttt{destruct {\term} as {\intropattern}}.
+
 \item{\tt destruct {\term} using {\qualid}}
 
   This is a synonym of {\tt induction {\term} using {\qualid}}.
@@ -1279,6 +1341,7 @@ components of an hypothesis.
 An introduction pattern is either:
 \begin{itemize}
 \item the wildcard: {\tt \_}
+\item the pattern \texttt{?}
 \item a variable
 \item a disjunction of lists of patterns:
   {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
@@ -1290,6 +1353,8 @@ structure of the pattern given as argument:
 \begin{itemize}
 \item introduction on the wildcard do the introduction and then
   immediately clear (cf~\ref{clear}) the corresponding hypothesis;
+\item introduction on \texttt{?} do the introduction, and let Coq
+  choose a fresh name for the variable;
 \item introduction on a variable behaves like described in~\ref{intro}; 
 \item introduction over a
 list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of
@@ -1323,7 +1388,8 @@ inductive type with a single constructor.
 Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
 intros A B C [a| [_ c]] f.
 apply (f a).
-Proof c.
+exact c.
+Qed.
 \end{coq_example}
 
 %\subsection{\tt FixPoint \dots}\tacindex{Fixpoint}
@@ -1479,7 +1545,10 @@ implicit type of $t$ and $u$.
 This tactic applies to any goal. The type of {\term}
 must have the form
 
-\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\term$_1${\tt =}\term$_2$. 
+\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\texttt{eq}\term$_1$ \term$_2$. 
+
+\noindent where \texttt{eq} is the Leibniz equality or a registered
+setoid equality.
 
 \noindent Then {\tt rewrite \term} replaces every occurrence of 
 \term$_1$ by \term$_2$ in the goal. Some of the variables x$_1$ are
@@ -1506,10 +1575,14 @@ This happens if \term$_1$ does not occur in the goal.
 \item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\
   Uses the equality \term$_1${\tt=}\term$_2$ from right to left
 
-\item {\tt rewrite {\term} in {\ident}}
+\item {\tt rewrite {\term} in \textit{clause}}
   \tacindex{rewrite \dots\ in}\\
-  Analogous to  {\tt rewrite {\term}} but rewriting is done in the
-  hypothesis named {\ident}.
+  Analogous to {\tt rewrite {\term}} but rewriting is done following
+  \textit{clause} (similarly to \ref{Conversion-tactics}). For instance:
+  \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H in H1;
+    rewrite H in H2; rewrite H} and \texttt{rewrite H in * |-} will do
+  \texttt{try rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <>
+    H}.
 
 \item {\tt rewrite -> {\term} in {\ident}}
   \tacindex{rewrite -> \dots\ in}\\
@@ -1540,17 +1613,26 @@ symmetric form occurs.  It is equivalent to {\tt cut
 \term$_2$=\term$_1$; [intro H{\sl n}; rewrite <- H{\sl n}; clear H{\sl
 n}| assumption || symmetry; try assumption]}.
 
+\begin{ErrMsgs}
+\item \errindex{terms do not have convertible types}
+\end{ErrMsgs}
+
 \begin{Variants}
   
 \item {\tt replace {\term$_1$} with {\term$_2$} in \ident}\\
   This replaces {\term$_1$} with {\term$_2$} in the hypothesis named
   {\ident}, and generates the subgoal {\term$_2$}{\tt =}{\term$_1$}. 
 
-  \begin{ErrMsgs}
-  \item \errindex{No such hypothesis} : {\ident}
-  \item \errindex{Nothing to rewrite in {\ident}}
-  \end{ErrMsgs}
+%   \begin{ErrMsgs}
+%   \item \errindex{No such hypothesis} : {\ident}
+%   \item \errindex{Nothing to rewrite in {\ident}}
+%   \end{ErrMsgs}
 
+\item {\tt replace {\term$_1$} with  {\term$_2$} by \tac}\\ This acts as
+  {\tt  replace {\term$_1$}  with {\term$_2$}}  but try  to  solve the
+  generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
+\item {\tt replace {\term$_1$} with {\term$_2$} in \ident by \tac}\\
+  This acts as {\tt replace {\term$_1$} with {\term$_2$} in \ident} but try to solve the generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
 \end{Variants}
 
 \subsection{\tt reflexivity
@@ -1617,12 +1699,12 @@ goal stating ``$eq$ {\term} {\term}$_1$''.
 Lemmas are added to the database using the command 
 \comindex{Declare Left Step}
 \begin{quote}
-{\tt Declare Left Step {\qualid}.}
+{\tt Declare Left Step {\term}.}
 \end{quote}
-where {\qualid} is the name of the lemma.
 
 The tactic is especially useful for parametric setoids which are not
-accepted as regular setoids for {\tt rewrite} and {\tt setoid\_replace} (see chapter \ref{setoid_replace}).
+accepted as regular setoids for {\tt rewrite} and {\tt
+  setoid\_replace} (see chapter \ref{setoid_replace}).
 
 \tacindex{stepr}
 \comindex{Declare Right Step}
@@ -1638,7 +1720,7 @@ Lemmas are expected to be of the form
 $z$, $R$ $x$ $y$ {\tt ->} $eq$ $y$ $z$ {\tt ->} $R$ $x$ $z$''
 and are registered using the command
 \begin{quote}
-{\tt Declare Right Step {\qualid}.}
+{\tt Declare Right Step {\term}.}
 \end{quote}
 \end{Variants}
 
@@ -2157,6 +2239,11 @@ hints of the database named {\tt core}.
   Uses all existing hint databases, minus the special database
   {\tt v62}. See Section~\ref{Hints-databases}
 
+\item \texttt{auto using $lemma_1, \ldots, lemma_n$}
+
+  Uses $lemma_1, \ldots, lemma_n$ in addition to hints (can be conbined
+  with the \texttt{with \ident} option).
+
 \item {\tt trivial}\tacindex{trivial}
 
   This tactic is a restriction of {\tt auto} that is not recursive and 
@@ -2306,6 +2393,15 @@ incompatibilities.
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
+
+\subsection{\tt rtauto
+\tacindex{rtauto}
+\label{rtauto}}
+
+The {\tt rtauto} tactic solves propositional tautologies similarly to what {\tt tauto} does. The main difference is that the proof term is built using a reflection scheme applied to a sequent calculus proof of the goal. The search procedure is also implemented using a different technique. 
+
+Users should be aware that this difference may result in faster proof-search but  slower proof-checking, and {\tt rtauto} might not solve goals that {\tt tauto} would be able to solve (e.g. goals involving universal quantifiers). 
+
 \subsection{{\tt firstorder}
 \tacindex{firstorder}
 \label{firstorder}}
@@ -2459,7 +2555,7 @@ equalities with uninterpreted symbols. It also include the constructor theory
 (see \ref{injection} and \ref{discriminate}).
 If the goal is a non-quantified equality, {\tt congruence} tries to
 prove it with non-quantified equalities in the context. Otherwise it
-tries to infer a discriminable equality from those in the context.
+tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that an hypothesis is equal to the goal or to the negation of another hypothesis.
 
 \begin{coq_eval}
 Reset Initial.
@@ -2489,14 +2585,28 @@ intros.
 congruence.
 \end{coq_example}
 
+\begin{Variants}
+\item {\tt congruence with \term$_1$ \dots\ \term$_n$}\\
+  Adds {\tt \term$_1$ \dots\ \term$_n$} to the pool of terms used by
+  {\tt congruence}. This helps in case you have partially applied
+  constructors in your goal.
+\end{Variants}
+
 \begin{ErrMsgs}
   \item \errindex{I don't know how to handle dependent equality} \\
     The decision procedure managed to find a proof of the goal or of
     a discriminable equality but this proof couldn't be built in Coq
     because of dependently-typed functions.
   \item \errindex{I couldn't solve goal} \\
-    The decision procedure didn't managed to find a proof of the goal or of
-    a discriminable equality.
+    The decision procedure didn't find any way to solve the goal.
+  \item \errindex{Goal is solvable by congruence but some arguments are missing. Try "congruence with \dots", replacing metavariables by arbitrary terms.} \\
+    The decision procedure could solve the goal with the provision
+    that additional arguments are supplied for some partially applied
+    constructors. Any term of an appropriate type will allow the
+    tactic to successfully solve the goal. Those additional arguments
+    can be given to {\tt congruence} by filling in the holes in the
+    terms given in the error message, using the {\tt with} variant
+    described below.
 \end{ErrMsgs}
 
 \subsection{\tt omega
@@ -2679,7 +2789,7 @@ of the reengineering of the code, this tactic has also been completely revised
 to get a very compact and readable version.} carries out rewritings according
 the rewriting rule bases {\tt \ident$_1$ \dots \ident$_n$}.
 
- Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until
+Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until
 it fails. Once all the rules have been processed, if the main subgoal has
 progressed (e.g., if it is distinct from the initial main goal) then the rules
 of this base are processed again. If the main subgoal has not progressed then
@@ -2695,58 +2805,24 @@ command.
 \item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\
 Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$
 $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
-%\item{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ]}\\
-%{\tt autorewrite  [ \ident$_1$ \dots \ident$_n$ ] using \tac}\\
-%These are deprecated syntactic variants for
-%{\tt autorewrite with \ident$_1$ \dots \ident$_n$}
-%and
-%{\tt autorewrite  with \ident$_1$ \dots \ident$_n$ using \tac}.
-\end{Variant}
 
-\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident
-\comindex{Hint Rewrite}}
+\item \texttt{autorewrite with {\ident} in {\qualid}}
 
-This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$}
-(their types must be equalities) in the rewriting base {\tt \ident}
-with the default orientation (left to right). Notice that the
-rewriting bases are distinct from the {\tt auto} hint bases and that
-{\tt auto} does not take them into account.
-
-This command is synchronous with the section mechanism (see \ref{Section}):
-when closing a section, all aliases created by \texttt{Hint Rewrite} in that
-section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite}
-declarations at the global level of that module are loaded.
-
-\begin{Variants}
-\item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\
-This is strictly equivalent to the command above (we only make explicit the
-orientation which otherwise defaults to {\tt ->}).
-
-\item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\
-Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left
-orientation in the base {\tt \ident}.
+  Performs all the rewritings in hypothesis {\qualid}.
 
-\item {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}\\
-When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will
-be used, the tactic {\tt \tac} will be applied to the generated subgoals, the
-main subgoal excluded.
-
-%% \item 
-%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\
-%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\
-%% These are deprecated syntactic variants for
-%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and
-%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}.
+\end{Variant}
 
-\end{Variants}
+\SeeAlso section \ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}.
 
-\SeeAlso \ref{autorewrite-example} for examples showing the use of
+\SeeAlso section \ref{autorewrite-example} for examples showing the use of
 this tactic. 
 
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v}
 
-\section{The hints databases for {\tt auto} and {\tt eauto}
+\section{Controlling automation}
+
+\subsection{The hints databases for {\tt auto} and {\tt eauto}
 \index{Hints databases}
 \label{Hints-databases}
 \comindex{Hint}}
@@ -3036,6 +3112,47 @@ every moment.
 
 \end{Variants}
 
+\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident
+\label{HintRewrite}
+\comindex{Hint Rewrite}}
+
+This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$}
+(their types must be equalities) in the rewriting base {\tt \ident}
+with the default orientation (left to right). Notice that the
+rewriting bases are distinct from the {\tt auto} hint bases and that
+{\tt auto} does not take them into account.
+
+This command is synchronous with the section mechanism (see \ref{Section}):
+when closing a section, all aliases created by \texttt{Hint Rewrite} in that
+section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite}
+declarations at the global level of that module are loaded.
+
+\begin{Variants}
+\item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\
+This is strictly equivalent to the command above (we only make explicit the
+orientation which otherwise defaults to {\tt ->}).
+
+\item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\
+Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left
+orientation in the base {\tt \ident}.
+
+\item {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}\\
+When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will
+be used, the tactic {\tt \tac} will be applied to the generated subgoals, the
+main subgoal excluded.
+
+%% \item 
+%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\
+%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\
+%% These are deprecated syntactic variants for
+%% {\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
 \label{Hint-and-Section}}
@@ -3046,6 +3163,42 @@ defined inside a section (and not defined with option {\tt Local}) become
 available when the module {\tt A} is imported (using
 e.g. \texttt{Require Import A.}).
 
+\subsection{Setting implicit automation tactics}
+
+\subsubsection{\tt Proof with {\tac}.}
+\label{ProofWith}
+\comindex{Proof with}
+
+  This command may be used to start a proof. It defines a default
+  tactic to be used each time a tactic command {\tac$_1$} is ended by
+  ``\verb#...#''. In this case the tactic command typed by the user is
+  equivalent to \tac$_1$;{\tac}.
+
+\SeeAlso {\tt Proof.} in section~\ref{BeginProof}.
+
+\subsubsection{\tt Declare Implicit Tactic {\tac}.}
+\comindex{Declare Implicit Tactic}
+
+This command declares a tactic to be used to solve implicit arguments
+that {\Coq} does not know how to solve by unification. It is used
+every time the term argument of a tactic has one of its holes not
+fully resolved.
+
+Here is an example:
+
+\begin{coq_example}
+Parameter quo : nat -> forall n:nat, n<>0 -> nat.
+Notation "x // y" := (quo x y _) (at level 40).
+
+Declare Implicit Tactic assumption.
+Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
+intros.
+exists (n // m).
+\end{coq_example}
+
+The tactic {\tt exists (n // m)} did not fail. The hole was solved by
+{\tt assumption} so that it behaved as {\tt exists (quo n m H)}.
+
 \section{Generation of induction principles with {\tt Scheme}
 \label{Scheme}
 \comindex{Scheme}}
@@ -3139,7 +3292,7 @@ The chapter~\ref{TacticLanguage} gives examples of more complex
 user-defined tactics.
 
 
-% $Id: RefMan-tac.tex 8938 2006-06-09 16:29:01Z jnarboux $ 
+% $Id: RefMan-tac.tex 9044 2006-07-12 13:22:17Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 4542e730..14fbff47 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -68,7 +68,7 @@
 \include{RefMan-oth.v}% Vernacular commands
 \include{RefMan-pro}% Proof handling
 \include{RefMan-tac.v}% Tactics and tacticals
-\include{RefMan-ltac}% Writing tactics
+\include{RefMan-ltac.v}% Writing tactics
 \include{RefMan-tacex.v}% Detailed Examples of tactics
 
 \part{User extensions}
@@ -122,4 +122,4 @@
 \end{document}
 
 
-% $Id: Reference-Manual.tex 8688 2006-04-07 15:08:12Z msozeau $ 
+% $Id: Reference-Manual.tex 9038 2006-07-11 13:53:53Z herbelin $ 
diff --git a/doc/refman/cover.html b/doc/refman/cover.html
index 1d2700b1..a3ec2516 100644
--- a/doc/refman/cover.html
+++ b/doc/refman/cover.html
@@ -13,7 +13,7 @@
 The Coq Proof Assistant<BR>
  Reference Manual<BR></B></FONT><FONT SIZE=7>
 </FONT>
-<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 8.0</B></FONT><FONT SIZE=5><B>
+<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 8.1</B></FONT><FONT SIZE=5><B>
 </B></FONT><A NAME="text1"></A><A HREF="#note1"><SUP><FONT SIZE=2>1</FONT></SUP></A><FONT SIZE=5><B><BR><BR><BR><BR><BR><BR>
 </B></FONT><FONT SIZE=5><B>The Coq Development Team</B></FONT><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>LogiCal Project</B></FONT><FONT SIZE=5><B><BR><BR><BR>
 </B></FONT></DIV><BR>
@@ -22,6 +22,7 @@ The Coq Proof Assistant<BR>
 <DIV ALIGN=left>
 <FONT SIZE=4>V7.x © INRIA 1999-2004</FONT><BR>
 <FONT SIZE=4>V8.0 © INRIA 2004-2006</FONT><BR>
+<FONT SIZE=4>V8.1 © INRIA 2006</FONT><BR>
 This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <A HREF="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</A>). Options A and B are not elected.
 </DIV>
 <BR>
diff --git a/doc/refman/index.html b/doc/refman/index.html
index db19678f..9b5250ab 100644
--- a/doc/refman/index.html
+++ b/doc/refman/index.html
@@ -1,29 +1,14 @@
 <HTML>
 
-<BODY>
+<HEAD>
 
-<CENTER>
+<TITLE>The Coq Proof Assistant Reference Manual</TITLE>
 
-<TABLE BORDER="0" CELLPADDING=10>
-<TR>
-<TD><CENTER><A HREF="cover.html" TARGET="UP"><FONT SIZE=2>Cover page</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="toc.html" TARGET="UP"><FONT SIZE=2>Table of contents</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="biblio.html" TARGET="UP"><FONT SIZE=2>
-Bibliography</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="general-index.html" TARGET="UP"><FONT SIZE=2>
-Global Index
-</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="tactic-index.html" TARGET="UP"><FONT SIZE=2>
-Tactics Index
-</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="command-index.html" TARGET="UP"><FONT SIZE=2>
-Vernacular Commands Index
-</FONT></A></CENTER></TD>
-<TD><CENTER><A HREF="error-index.html" TARGET="UP"><FONT SIZE=2>
-Index of Error Messages
-</FONT></A></CENTER></TD>
-</TABLE>
+</HEAD>
 
-</CENTER>
+<FRAMESET ROWS=90%,*>
+  <FRAME SRC="cover.html" NAME="UP">
+  <FRAME SRC="menu.html">
+</FRAMESET>
 
-</BODY></HTML>
\ No newline at end of file
+</HTML>
\ No newline at end of file
diff --git a/doc/refman/menu.html b/doc/refman/menu.html
new file mode 100644
index 00000000..db19678f
--- /dev/null
+++ b/doc/refman/menu.html
@@ -0,0 +1,29 @@
+<HTML>
+
+<BODY>
+
+<CENTER>
+
+<TABLE BORDER="0" CELLPADDING=10>
+<TR>
+<TD><CENTER><A HREF="cover.html" TARGET="UP"><FONT SIZE=2>Cover page</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="toc.html" TARGET="UP"><FONT SIZE=2>Table of contents</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="biblio.html" TARGET="UP"><FONT SIZE=2>
+Bibliography</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="general-index.html" TARGET="UP"><FONT SIZE=2>
+Global Index
+</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="tactic-index.html" TARGET="UP"><FONT SIZE=2>
+Tactics Index
+</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="command-index.html" TARGET="UP"><FONT SIZE=2>
+Vernacular Commands Index
+</FONT></A></CENTER></TD>
+<TD><CENTER><A HREF="error-index.html" TARGET="UP"><FONT SIZE=2>
+Index of Error Messages
+</FONT></A></CENTER></TD>
+</TABLE>
+
+</CENTER>
+
+</BODY></HTML>
\ No newline at end of file
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 73d833c4..d5523f1f 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -31,20 +31,29 @@ proof tools.  For more advanced information, the reader could refer to
 the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y.
 Bertot and P. Castéran on practical uses of the \Coq{} system.
 
-We assume here that the potential user has installed \Coq~ on his workstation,
-that he calls \Coq~ from a standard teletype-like shell window, and that
-he does not use any special interface.
+Coq can be used from a standard teletype-like shell window but
+preferably through the graphical user interface
+CoqIde\footnote{Alternative graphical interfaces exist: Proof General
+and Pcoq.}.
+
 Instructions on installation procedures, as well as more comprehensive
 documentation, may be found in the standard distribution of \Coq,
 which may be obtained from \Coq{} web site \texttt{http://coq.inria.fr}.
 
-In the following, all examples preceded by the prompting sequence
-\verb:Coq < : represent user input, terminated by a period. The
-following lines usually show \Coq's answer as it appears on the users
-screen. The sequence of such examples is a valid \Coq~ session, unless
-otherwise specified. This version of the tutorial has been prepared 
-on a PC workstation running Linux.
-The standard invocation of \Coq\ delivers a message such as:
+In the following, we assume that \Coq~ is called from a standard
+teletype-like shell window. All examples preceded by the prompting
+sequence \verb:Coq < : represent user input, terminated by a
+period. 
+
+The following lines usually show \Coq's answer as it appears on the
+users screen. When used from a graphical user interface such as
+CoqIde, the prompt is not displayed: user input is given in one window
+and \Coq's answers are displayed in a different window.
+
+The sequence of such examples is a valid \Coq~
+session, unless otherwise specified. This version of the tutorial has
+been prepared on a PC workstation running Linux.  The standard
+invocation of \Coq\ delivers a message such as:
 
 \begin{small}
 \begin{flushleft}
@@ -1552,4 +1561,4 @@ with \Coq, in order to acquaint yourself with various proof techniques.
 
 \end{document}
 
-% $Id: Tutorial.tex 8715 2006-04-14 12:43:23Z cpaulin $ 
+% $Id: Tutorial.tex 8978 2006-06-23 10:15:57Z herbelin $