- Extension de "generalize" en "generalize c as id at occs".

- Ajout clause "in" à "remember" (et passage du code en ML).
- Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute
  aussi une égalité pour se souvenir du terme sur lequel l'induction
  ou l'analyse de cas s'applique.
- Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de
  Programs qui avait la sémantique de "pose proof" tandis que le nouveau
  a la même sémantique que "pose (id:=t)").
- Un peu de réorganisation, uniformisation de noms dans Arith, et
  ajout EqNat dans Arith.
- Documentation tactiques et notations de tactiques.



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

3 files changed, 244 insertions, 146 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 6b6c158b5..1c4fa7e1f 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -125,7 +125,9 @@
 \newcommand{\caseitem}{\nterm{match\_item}}
 \newcommand{\eqn}{\nterm{equation}}
 \newcommand{\ifitem}{\nterm{dep\_ret\_type}}
-\newcommand{\letclauses}{\nterm{letclauses}}
+\newcommand{\convclause}{\nterm{conversion\_clause}}
+\newcommand{\occclause}{\nterm{occurrence\_clause}}
+\newcommand{\occset}{\nterm{occurrence\_set}}
 \newcommand{\params}{\nterm{params}} % vernac
 \newcommand{\returntype}{\nterm{return\_type}}
 \newcommand{\idparams}{\nterm{ident\_with\_params}}
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 71e87b3f3..e319bdbb1 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -1002,14 +1002,23 @@ syntax
 %{\tt preident} $|$
 {\tt ident} $|$
 {\tt simple\_intropattern} $|$
-{\tt hyp} \\ & $|$ &
-% {\tt quantified\_hypothesis} $|$
-{\tt reference} $|$
-{\tt constr} \\ & $|$ &
+{\tt reference} \\ & $|$ &
+{\tt hyp} $|$
+{\tt hyp\_list} $|$
+{\tt ne\_hyp\_list} \\ & $|$ &
+% {\tt quantified\_hypothesis} \\ & $|$ &
+{\tt constr} $|$
+{\tt constr\_list} $|$
+{\tt ne\_constr\_list} \\ & $|$ &
 %{\tt castedopenconstr} $|$
 {\tt integer} $|$
-{\tt int\_or\_var} \\ & $|$ &
+{\tt integer\_list} $|$
+{\tt ne\_integer\_list} \\ & $|$ &
+{\tt int\_or\_var} $|$
+{\tt int\_or\_var\_list} $|$
+{\tt ne\_int\_or\_var\_list} \\ & $|$ &
 {\tt tactic} $|$ {\tt tactic$n$} \qquad\mbox{(for $0\leq n\leq 5$)}
+
 \end{tabular}
 \medskip
 
@@ -1034,7 +1043,7 @@ use the corresponding kind of argument.
 \noindent
 \begin{tabular}{l|l|l|l}
 Tactic argument type & parsed as & interpreted as & as in tactic \\
-\hline \\
+\hline & & & \\
 {\tt\small ident} & identifier & a user-given name & {\tt intro} \\
 {\tt\small simple\_intropattern} & intro\_pattern & an intro\_pattern & {\tt intros}\\
 {\tt\small hyp} & identifier & an hypothesis defined in context & {\tt clear}\\
@@ -1046,8 +1055,10 @@ Tactic argument type & parsed as & interpreted as & as in tactic \\
 %%{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\
 {\tt\small integer} & integer & an integer &  \\
 {\tt\small int\_or\_var} & identifier or integer & an integer & {\tt do} \\
-{\tt\small tactic} & tactic at level 5 & a tactic & \\
+{\tt\small tactic} & tactic at level 5 & a tactic &  \\
 {\tt\small tactic$n$} & tactic at level $n$ & a tactic & \\
+{\tt\small {\nterm{entry}}\_list} & list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted & \\
+{\tt\small ne\_{\nterm{entry}}\_list} & non-empty list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted& \\
 \end{tabular}
 
 \Rem In order to be bound in tactic definitions, each syntactic entry
@@ -1059,6 +1070,12 @@ for {\tt integer}. This is the reason for introducing a special entry
 syntactically includes identifiers in order to be usable in tactic
 definitions.
 
+\Rem The {\tt {\nterm{entry}}\_list} and {\tt ne\_{\nterm{entry}}\_list}
+entries can be used in primitive tactics or in other notations at
+places where a list of the underlying entry can be used: {\nterm{entry}} is
+either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or
+{\tt\small int\_or\_var}.
+
 % $Id$ 
 
 %%% Local Variables: 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 3a8f6ca52..45993dd23 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -437,7 +437,8 @@ Section~\ref{pattern} to transform the goal so that it gets the form
 \subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )}
 \label{tactic:set}
 \tacindex{set}
-\tacindex{pose}}
+\tacindex{pose}
+\tacindex{remember}}
 
 This replaces {\term} by {\ident} in the conclusion or in the
 hypotheses of the current goal and adds the new definition {\ident
@@ -446,81 +447,45 @@ replacement only in the conclusion.
 
 \begin{Variants}
 
-\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *}\\
-  {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |- *}\\
-  
-  This behaves as above but substitutes {\term}
-  everywhere in the goal (both in conclusion and hypotheses).
-
-\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |-}
-  
-  This behaves the same but substitutes {\term} in
-  the hypotheses only (not in the conclusion).
-
-\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- *}
-  
-  This is equivalent to {\tt set ( } {\ident} {\tt :=} {\term} {\tt
-  )}, i.e. it substitutes {\term} in the conclusion only.
-
-\item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}}
-  
-  This behaves the same but substitutes {\term} only in
-  the hypothesis named {\ident$_1$}.
-  
-\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
-    {\ident$_1$} {\tt at} {\num$_1$} \dots\ {\num$_n$}
+\item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occset}}
 
 This notation allows to specify which occurrences of {\term} have to
-be substituted in the hypothesis named {\ident$_1$}. The occurrences
-are numbered from left to right and are meaningful on a pure
-expression using no implicit argument, notation or coercion. A
-negative occurrence number means an occurrence which should not be
-substituted. As an exception of the left-to-right order, the
-occurrences in the {\tt return} subexpression of a {\tt match} are
-considered {\em before} the occurrences in the matched term.
-
-For expressions using notations, or hiding implicit arguments or
-coercions, it is recommended to make explicit all occurrences in 
-order by using {\tt Set Printing All} (see
-section~\ref{SetPrintingAll}).
-
-\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- * at}
-      {\num$_1$} \dots\ {\num$_n$}
-  
-This allows to specify which occurrences of the conclusion are concerned.
-
-\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
-    {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots
-    {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}
-  
-  It substitutes {\term} at occurrences {\num$_1^i$} \dots\
-  {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. Each {\tt at} part is
-  optional.
+be substituted in the context. The {\tt in {\occset}} clause is an
+occurrence clause whose syntax and behavior is described in
+Section~\ref{Occurrences clauses}.
 
 \item {\tt set (} {\ident} \nelist{\binder}{} {\tt :=} {\term} {\tt )}
 
   This is equivalent to {\tt set (} {\ident} {\tt :=} {\tt fun}
   \nelist{\binder}{} {\tt =>} {\term} {\tt )}.
 
-\item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term} {\tt ) in}
-    {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots
-    {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}
-    {\tt |- *} {\tt at} {\num$'_1$} \dots\ {\num$'_n$}
-
-  This is the more general form which combines all the previous
-  possibilities.
-
 \item {\tt set } {\term}
 
   This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident}
-    is generated by {\Coq}. This variant is available for the 
-    forms with {\tt in} too.
+  is generated by {\Coq}. This variant also supports an occurrence clause.
+
+\item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term}
+      {\tt ) in {\occset}}\\
+      {\tt set {\term} in {\occset}}
+
+  These are the general forms which combine the previous possibilities.
+
+\item {\tt remember {\term} {\tt as} {\ident}}
+
+  This behaves as {\tt set (} {\ident} := {\term} {\tt ) in *} and using a
+  logical (Leibniz's) equality instead of a local definition.
+
+\item {\tt remember {\term} {\tt as} {\ident} in {\occset}}
+
+  This is a more general form of {\tt remember} that remembers the
+  occurrences of {\term} specified by an occurrences set.
 
 \item {\tt pose (  {\ident} {\tt :=} {\term} {\tt )}}
   
   This adds the local definition {\ident} := {\term} to the current
   context without performing any replacement in the goal or in the
-  hypotheses.
+  hypotheses. It is equivalent to {\tt set ( {\ident} {\tt :=}
+  {\term} {\tt ) in |-}}.
 
 \item {\tt pose (} {\ident} \nelist{\binder}{} {\tt :=} {\term} {\tt )}
 
@@ -528,7 +493,7 @@ This allows to specify which occurrences of the conclusion are concerned.
   \nelist{\binder}{} {\tt =>} {\term} {\tt )}.
 
 \item{\tt pose {\term}}
-  
+
   This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but
   {\ident} is generated by {\Coq}.
 
@@ -687,11 +652,31 @@ where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by
 to $T$.
 
 \begin{Variants}
-\item {\tt generalize \term$_1$ \dots\ \term$_n$} 
+\item {\tt generalize {\term$_1$ , \dots\ , \term$_n$}}
   
   Is equivalent to {\tt generalize \term$_n$; \dots\ ; generalize
     \term$_1$}. Note that the sequence of \term$_i$'s are processed
   from $n$ to $1$.
+
+\item {\tt generalize {\term} at {\num$_1$ \dots\ \num$_i$}}
+  
+  Is equivalent to {\tt generalize \term} but generalizing only over
+  the specified occurrences of {\term} (counting from left to right on the
+  expression printed using option {\tt Set Printing All}).
+
+\item {\tt generalize {\term} as {\ident}}
+  
+  Is equivalent to {\tt generalize \term} but use {\ident} to name the
+  generalized hypothesis.
+
+\item {\tt generalize {\term$_1$} at {\num$_{11}$ \dots\ \num$_{1i_1}$} 
+                      as {\ident$_1$}
+                      , {\ldots} ,
+                      {\term$_n$} at {\num$_{n1}$ \dots\ \num$_{ni_n}$}
+                      as {\ident$_2$}}
+  
+  This is the most general form of {\tt generalize} that combines the
+  previous behaviors.
   
 \item {\tt generalize dependent \term} \tacindex{generalize dependent}
   
@@ -701,7 +686,7 @@ to $T$.
 \item {\tt revert \ident$_1$ \dots\ \ident$_n$}\tacindex{revert}
  
   This is equivalent to a {\tt generalize} followed by a {\tt clear}
-  on the given hypotheses. This tactic can be seem as reciprocal to 
+  on the given hypotheses. This tactic can be seen as reciprocal to 
   {\tt intros}. 
 
 \end{Variants}
@@ -748,44 +733,6 @@ This tactic applies to any goal. It implements the rule
 \end{Variants}
 
 \SeeAlso \ref{Conversion-tactics}
-\subsection{Bindings list
-\index{Binding list}
-\label{Binding-list}}
-
-Tactics that take a term as argument may also support bindings list so
-as to instantiate some parameters of the term by name or position.
-The general form of a term equipped with a bindings list is {\tt
-{\term} with {\bindinglist}} where {\bindinglist} may be of two
-different forms:
-
-\begin{itemize}
-\item In a bindings list of the form {\tt (\vref$_1$ := \term$_1$)
-  \dots\ (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a
-  {\num}. The references are determined according to the type of
-  {\term}. If \vref$_i$ is an identifier, this identifier has to be
-  bound in the type of {\term} and the binding provides the tactic
-  with an instance for the parameter of this name.  If \vref$_i$ is
-  some number $n$, this number denotes the $n$-th non dependent
-  premise of the {\term}, as determined by the type of {\term}.
-
-  \ErrMsg \errindex{No such binder}
-
-\item A bindings list can also be a simple list of terms {\tt
-  \term$_1$ \term$_2$ \dots\term$_n$}. In that case the references to
-  which these terms correspond are determined by the tactic. In case
-  of {\tt induction}, {\tt destruct}, {\tt elim} and {\tt case} (see
-  Section~\ref{elim}) the terms have to provide instances for all the
-  dependent products in the type of \term\ while in the case of {\tt
-  apply}, or of {\tt constructor} and its variants, only instances for
-  the dependent products which are not bound in the conclusion of the
-  type are required.
-
-  \ErrMsg \errindex{Not the right number of missing arguments}
-
-\end{itemize}
-
-
-
 \subsection{\tt evar (\ident:\term)
 \tacindex{evar}
 \label{evar}}
@@ -887,6 +834,101 @@ simultaneously proved are respectively {\tt forall}
 
 \end{Variants}
 
+\subsection{Bindings list
+\index{Binding list}
+\label{Binding-list}}
+
+Tactics that take a term as argument may also support bindings list so
+as to instantiate some parameters of the term by name or position.
+The general form of a term equipped with a bindings list is {\tt
+{\term} with {\bindinglist}} where {\bindinglist} may be of two
+different forms:
+
+\begin{itemize}
+\item In a bindings list of the form {\tt (\vref$_1$ := \term$_1$)
+  \dots\ (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a
+  {\num}. The references are determined according to the type of
+  {\term}. If \vref$_i$ is an identifier, this identifier has to be
+  bound in the type of {\term} and the binding provides the tactic
+  with an instance for the parameter of this name.  If \vref$_i$ is
+  some number $n$, this number denotes the $n$-th non dependent
+  premise of the {\term}, as determined by the type of {\term}.
+
+  \ErrMsg \errindex{No such binder}
+
+\item A bindings list can also be a simple list of terms {\tt
+  \term$_1$ \dots\term$_n$}. In that case the references to
+  which these terms correspond are determined by the tactic. In case
+  of {\tt induction}, {\tt destruct}, {\tt elim} and {\tt case} (see
+  Section~\ref{elim}) the terms have to provide instances for all the
+  dependent products in the type of \term\ while in the case of {\tt
+  apply}, or of {\tt constructor} and its variants, only instances for
+  the dependent products which are not bound in the conclusion of the
+  type are required.
+
+  \ErrMsg \errindex{Not the right number of missing arguments}
+
+\end{itemize}
+
+\subsection{Occurrences sets and occurrences clauses}
+\label{Occurrences clauses}
+\index{Occurrences clauses}
+
+An occurrences clause is a modifier to some tactics that obeys the
+following syntax:
+
+$\!\!\!$\begin{tabular}{lcl}
+{\occclause} & ::= & {\tt in} {\occset} \\
+{\occset} & ::= &
+    \zeroone{{\ident$_1$} \zeroone{{\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}} {\tt ,} {\dots} {\tt ,}
+    {\ident$_m$} \zeroone{{\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}}}\\
+&   &
+    \zeroone{{\tt |-} 
+      \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}}\\
+& | &
+    {\tt *} {\tt |-}
+        \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}\\
+& | &
+    {\tt *}\\
+\end{tabular}
+
+The role of an occurrence clause is to select a set of occurrences of
+a {\term} in a goal. In the first case, the {{\ident$_i$}
+\zeroone{{\tt at} {\num$_1^i$} \dots\ {\num$_{n_i}^i$}}} parts
+indicate that occurrences have to be selected in the hypotheses named
+{\ident$_i$}.  If no numbers are given for hypothesis {\ident$_i$},
+then all occurrences of {\term} in the hypothesis are selected. If
+numbers are given, they refer to occurrences of {\term} when the term
+is printed using option {\tt Set Printing All} (see
+Section~\ref{SetPrintingAll}), counting from left to right. In
+particular, occurrences of {\term} in implicit arguments (see
+Section~\ref{Implicit Arguments}) or coercions (see
+Section~\ref{Coercions}) are counted.
+
+A negative occurrence number means an occurrence which should not be
+substituted.  As an exception to the left-to-right order, the
+occurrences in the {\tt return} subexpression of a {\tt match} are
+considered {\em before} the occurrences in the matched term.
+
+In the second case, the {\tt *} on the left of {\tt |-} means that
+all occurrences of {\term} are selected in every hypothesis.
+
+In the first and second case, if {\tt *} is mentioned on the right of
+{\tt |-}, the occurrences of the conclusion of the goal have to be
+selected. If some numbers are given, then only the occurrences denoted
+by these numbers are selected. In no numbers are given, all
+occurrences of {\term} in the goal are selected.
+
+Finally, the last notation is an abbreviation for {\tt * |- *}. Note
+also that {\tt |-} is optional in the first case when no {\tt *} is
+given.
+
+Here are some tactics that understand occurrences clauses:
+{\tt set}, {\tt remember}, {\tt induction}, {\tt destruct}.
+
+\SeeAlso~Sections~\ref{tactic:set}, \ref{Tac-induction}, \ref{SetPrintingAll}.
+
+
 \section{Negation and contradiction}
 
 \subsection{\tt absurd \term
@@ -945,32 +987,35 @@ tactic \texttt{change}.
 
 All conversion tactics (including \texttt{change}) can be
 parameterized by the parts of the goal where the conversion can
-occur. The specification of such parts are called \emph{clauses}. It
-can be either the conclusion, or an hypothesis. In the case of a
-defined hypothesis it is possible to specify if the conversion should
-occur on the type part, the body part or both (default).
-
-\index{Clauses} Clauses are written after a conversion tactic (tactics
+occur. This is done using \emph{goal clauses} which consists in a list
+of hypotheses and, optionally, of a reference to the conclusion of the
+goal. For defined hypothesis it is possible to specify if the
+conversion should occur on the type part, the body part or both
+(default).
+
+\index{Clauses}
+\index{Goal clauses}
+Goal clauses are written after a conversion tactic (tactics
 \texttt{set}~\ref{tactic:set},          \texttt{rewrite}~\ref{rewrite},
 \texttt{replace}~\ref{tactic:replace}                               and
 \texttt{autorewrite}~\ref{tactic:autorewrite}  also  use clauses)  and
-are introduced by  the keyword \texttt{in}. If no  clause is provided,
+are introduced by  the keyword \texttt{in}. If no goal clause is provided,
 the default is to perform the conversion only in the conclusion.
 
-The syntax and description of the various clauses follows:
+The syntax and description of the various goal clauses is the following:
 \begin{description}
-\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- }] only in hypotheses $H_1
-  $\ldots$ H_n$
-\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- *}] in hypotheses $H_1 \ldots
-  H_n$ and in the conclusion
-\item[\texttt{in * |-}] in every hypothesis
-\item[\texttt{in *}] (equivalent to \texttt{in * |- *}) everywhere
-\item[\texttt{in (type of H$_1$) (value of H$_2$) $\ldots$ |-}] in
-  type part of $H_1$, in the value part of $H_2$, etc. 
+\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- } only in hypotheses {\ident}$_1$
+  \ldots {\ident}$_n$
+\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- *} in hypotheses {\ident}$_1$ \ldots
+  {\ident}$_n$ and in the conclusion
+\item[]\texttt{in * |-} in every hypothesis
+\item[]\texttt{in *} (equivalent to \texttt{in * |- *}) everywhere
+\item[]\texttt{in (type of {\ident}$_1$) (value of {\ident}$_2$) $\ldots$ |-} in
+  type part of {\ident}$_1$, in the value part of {\ident}$_2$, etc. 
 \end{description}
 
-For backward compatibility, the notation \texttt{in}~$H_1\ldots H_n$
-performs the conversion in hypotheses $H_1\ldots H_n$.
+For backward compatibility, the notation \texttt{in}~{\ident}$_1$\ldots {\ident}$_n$
+performs the conversion in hypotheses {\ident}$_1$\ldots {\ident}$_n$.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %voir reduction__conv_x : histoires d'univers.
@@ -1451,12 +1496,28 @@ induction n.
   with complex predicates as the induction principles generated by
   {\tt Function} or {\tt Functional Scheme} may be.
 
-\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\
-     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}
+\item \texttt{induction {\term} in *}
+
+  This syntax tells to keep an equation between {\term} and the value
+  it gets in each case of the induction.
+
+\item \texttt{induction {\term} in {\occset}}
+
+  This syntax is used for selecting which occurrences of {\term} the
+  induction has to be carried on. The {\tt in {\occset}} clause is an
+  occurrence clause whose syntax and behavior is described in
+  Section~\ref{Occurrences clause}.
 
-  This is the most general form of {\tt induction} and {\tt einduction}.
-  It combines the effects of the {\tt with}, {\tt as}, and {\tt
-  using} clauses.
+  When an occurrence clause is given, an equation between {\term} and
+  the value it gets in each case of the induction is added to the
+  context of the subgoals corresponding to the induction cases.
+
+\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\
+     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}
+
+  This is the most general form of {\tt induction} and {\tt
+  einduction}.  It combines the effects of the {\tt with}, {\tt as},
+  {\tt using}, and {\tt in} clauses.
 
 \item {\tt elim \term}\label{elim}
   
@@ -1611,12 +1672,28 @@ last introduced hypothesis.
   These are synonyms of {\tt induction {\term$_1$} using {\term$_2$}} and
   {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}}.
 
-\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\
-     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\
+\item \texttt{destruct {\term} in *}
+
+  This syntax tells to keep an equation between {\term} and the value
+  it gets in each cases of the analysis.
+
+\item \texttt{destruct {\term} in {\occset}}
+
+  This syntax is used for selecting which occurrences of {\term} the
+  case analysis has to be done on. The {\tt in {\occset}} clause is an
+  occurrence clause whose syntax and behavior is described in
+  Section~\ref{Occurrences clauses}.
+
+  When an occurrence clause is given, an equation between {\term} and
+  the value it gets in each cases of the analysis is added to the
+  context of the subgoals corresponding to the cases.
+
+\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\
+     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}
 
   This is the most general form of {\tt destruct} and {\tt edestruct}.
-  It combines the effects of the {\tt with}, {\tt as}, and {\tt
-  using} clauses.
+  It combines the effects of the {\tt with}, {\tt as}, {\tt using},
+  and {\tt in} clauses.
 
 \item{\tt case \term}\label{case}\tacindex{case}
   
@@ -1627,10 +1704,12 @@ last introduced hypothesis.
 \item{\tt case\_eq \term}\label{case_eq}\tacindex{case\_eq}
 
  The tactic {\tt case\_eq} is a variant of the {\tt case} tactic that
- allow to perform case analysis on a term without completely 
- forgetting its original form. This is done by generating 
- equalities between the original form of the term and the outcomes of 
- the case analysis. 
+ allow to perform case analysis on a term without completely
+ forgetting its original form. This is done by generating equalities
+ between the original form of the term and the outcomes of the case
+ analysis. The effect of this tactic is similar to the effect of {\tt
+ destruct {\term} in |- *} to the exception that no new hypotheses 
+ is introduced in the context.
 
 \item {\tt case {\term} with {\bindinglist}}
 
@@ -2063,7 +2142,7 @@ This happens if \term$_1$ does not occur in the goal.
   Rewrite only the given occurrences of \term$_1'$. Occurrences are
   specified from left to right as for \texttt{pattern} (\S
   \ref{pattern}). The rewrite is always performed using setoid
-  rewriting, even for leibniz equality, so one has to 
+  rewriting, even for Leibniz's equality, so one has to 
   \texttt{Import Setoid} to use this variant.
 
 \item {\tt rewrite {\term} by {\tac}}
@@ -2379,7 +2458,7 @@ Abort.
 Beware that \texttt{injection} yields always an equality in a sigma type
 whenever the injected object has a dependent type.
 
-\Rem There is a special case for dependant pairs. If we have a decidable 
+\Rem There is a special case for dependent pairs. If we have a decidable 
 equality over the type of the first argument, then it is safe to do 
 the projection on the second one, and so {\tt injection} will work fine.
 To define such an equality, you have to use the {\tt Scheme} command 
@@ -2521,7 +2600,7 @@ latter is first introduced in the local context using
   on the equalities it generates), the corresponding name $p_{ij}$ in
   the list must be replaced by a sublist of the form {\tt [$p_{ij1}$
   \ldots $p_{ijq}$]} (or, equivalently, {\tt ($p_{ij1}$,
-  \ldots, $p_{ijq}$)}) where $q$ is the number of subequations
+  \ldots, $p_{ijq}$)}) where $q$ is the number of subequalities
   obtained from splitting the original equation. Here is an example.
 
 \begin{coq_eval}
@@ -3502,7 +3581,7 @@ Require Import List.
 \end{coq_example*}
 \begin{coq_example}
 Hint Extern 5   ({?X1 = ?X2} + {?X1 <> ?X2}) =>
- generalize X1 X2; decide equality : eqdec.
+ generalize X1, X2; decide equality : eqdec.
 Goal 
 forall a b:list (nat * nat), {a = b} + {a <> b}.
 info auto with eqdec.
@@ -3774,7 +3853,7 @@ general principle of mutual induction for objects in type {\term$_i$}.
 \subsection{Automatic declaration of schemes}
 \comindex{Set Equality Scheme}
 \comindex{Set Elimination Schemes}
-It is possible to desactive the automatic declaration of the induction
+It is possible to deactivate the automatic declaration of the induction
  principles when defining a new inductive type  with the
  {\tt UnSet Elimination Schemes} command. It may be
 reactivated at any time with {\tt Set Elimination Schemes}. 
@@ -3782,7 +3861,7 @@ reactivated at any time with {\tt Set Elimination Schemes}.
 
 You can also activate the automatic declaration of those boolean equalities 
 (see the second variant of {\tt Scheme})  with the {\tt Set Equality Scheme}
- command. However you have to be carefull with this option since
+ command. However you have to be careful with this option since
 \Coq~ may now reject well-defined inductive types because it cannot compute
 a boolean equality for them.