Imported Upstream version 8.3upstream/8.3

1 files changed, 4303 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
new file mode 100644
index 00000000..b82cdc2d
--- /dev/null
+++ b/doc/refman/RefMan-tac.tex
@@ -0,0 +1,4303 @@
+% TODO: unify the use of \form and \type to mean a type
+% or use \form specifically for a type of type Prop
+\chapter{Tactics
+\index{Tactics}
+\label{Tactics}}
+
+A deduction rule is a link between some (unique) formula, that we call
+the {\em conclusion} and (several) formulas that we call the {\em
+premises}. Indeed, a deduction rule can be read in two ways. The first
+one has the shape: {\it ``if I know this and this then I can deduce
+this''}. For instance, if I have a proof of $A$ and a proof of $B$
+then I have a proof of $A \land B$. This is forward reasoning from
+premises to conclusion. The other way says: {\it ``to prove this I
+have to prove this and this''}. For instance, to prove $A \land B$, I
+have to prove $A$ and I have to prove $B$. This is backward reasoning
+which proceeds from conclusion to premises. We say that the conclusion
+is {\em the goal}\index{goal} to prove and premises are {\em the
+subgoals}\index{subgoal}.  The tactics implement {\em backward
+reasoning}. When applied to a goal, a tactic replaces this goal with
+the subgoals it generates. We say that a tactic reduces a goal to its
+subgoal(s).
+
+Each (sub)goal is denoted with a number. The current goal is numbered
+1. By default, a tactic is applied to the current goal, but one can
+address a particular goal in the list by writing {\sl n:\tac} which
+means {\it ``apply tactic {\tac} to goal number {\sl n}''}.
+We can show the list of subgoals by typing {\tt Show} (see
+Section~\ref{Show}). 
+
+Since not every rule applies to a given statement, every tactic cannot be
+used to reduce any goal. In other words, before applying a tactic to a
+given goal, the system checks that some {\em preconditions} are
+satisfied. If it is not the case, the tactic raises an error message.
+
+Tactics are build from atomic tactics and tactic expressions (which
+extends the folklore notion of tactical) to combine those atomic
+tactics. This chapter is devoted to atomic tactics. The tactic
+language will be described in Chapter~\ref{TacticLanguage}.
+
+There are, at least, three levels of atomic tactics. The simplest one
+implements basic rules of the logical framework. The second level is
+the one of {\em derived rules} which are built by combination of other
+tactics. The third one implements heuristics or decision procedures to
+build a complete proof of a goal.
+
+\section{Invocation of tactics
+\label{tactic-syntax}
+\index{tactic@{\tac}}}
+
+A tactic is applied as an ordinary command. If the tactic does not
+address the first subgoal, the command may be preceded by the wished
+subgoal number as shown below:
+
+\begin{tabular}{lcl}
+{\commandtac} & ::= & {\num} {\tt :} {\tac} {\tt .}\\
+ & $|$ & {\tac} {\tt .}
+\end{tabular}
+
+\section{Explicit proof as a term}
+
+\subsection{\tt exact \term
+\tacindex{exact}
+\label{exact}}
+
+This tactic applies to any goal. It gives directly the exact proof
+term of the goal. Let {\T} be our goal, let {\tt p} be a term of type
+{\tt U} then {\tt exact p} succeeds iff {\tt T} and {\tt U} are
+convertible (see Section~\ref{conv-rules}).
+
+\begin{ErrMsgs}
+\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}
+\label{refine}
+\index{?@{\texttt{?}}}}
+
+This tactic allows to give an exact proof but still with some
+holes. The holes are noted ``\texttt{\_}''.
+
+\begin{ErrMsgs}
+\item \errindex{invalid argument}: 
+  the tactic \texttt{refine} doesn't know what to do
+  with the term you gave.
+\item \texttt{Refine passed ill-formed term}: the term you gave is not
+  a valid proof (not easy to debug in general).
+  This message may also occur in higher-level tactics, which call 
+  \texttt{refine} internally.
+\item \errindex{Cannot infer a term for this placeholder}
+  there is a hole in the term you gave
+  which type cannot be inferred. Put a cast around it.
+\end{ErrMsgs}
+
+An example of use is given in Section~\ref{refine-example}.
+
+\section{Basics
+\index{Typing rules}}
+
+Tactics presented in this section implement the basic typing rules of
+{\CIC} given in Chapter~\ref{Cic}.
+
+\subsection{{\tt assumption}
+\tacindex{assumption}}
+
+This tactic applies to any goal. It implements the
+``Var''\index{Typing rules!Var} rule given in
+Section~\ref{Typed-terms}. It looks in the local context for an
+hypothesis which type is equal to the goal.  If it is the case, the
+subgoal is proved. Otherwise, it fails.
+
+\begin{ErrMsgs}
+\item  \errindex{No such assumption}
+\end{ErrMsgs}
+
+\begin{Variants}
+\tacindex{eassumption}
+  \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}}
+
+This tactic erases the hypothesis named {\ident} in the local context
+of the current goal. Then {\ident} is no more displayed and no more
+usable in the proof development.
+
+\begin{Variants}
+
+\item {\tt clear {\ident$_1$} {\ldots} {\ident$_n$}}
+  
+  This is equivalent to {\tt clear {\ident$_1$}. {\ldots} clear
+    {\ident$_n$}.}
+  
+\item {\tt clearbody {\ident}}\tacindex{clearbody}
+
+  This tactic expects {\ident} to be a local definition then clears
+  its body. Otherwise said, this tactic turns a definition into an
+  assumption.
+
+\item \texttt{clear - {\ident$_1$} {\ldots} {\ident$_n$}}
+
+  This tactic clears all hypotheses except the ones depending in 
+  the hypotheses named {\ident$_1$} {\ldots} {\ident$_n$} and in the
+  goal.
+
+\item \texttt{clear}
+
+  This tactic clears all hypotheses except the ones depending in 
+  goal.
+
+\item {\tt clear dependent \ident \tacindex{clear dependent}}
+
+ This clears the hypothesis \ident\ and all hypotheses
+ which depend on it.
+
+\end{Variants}
+
+\begin{ErrMsgs}
+\item \errindex{{\ident} not found}
+\item \errindexbis{{\ident} is used in the conclusion}{is used in the
+    conclusion} 
+\item \errindexbis{{\ident} is used in the hypothesis {\ident'}}{is
+    used in the hypothesis} 
+\end{ErrMsgs}
+
+\subsection{\tt move {\ident$_1$} after {\ident$_2$}
+\tacindex{move}
+\label{move}}
+
+This moves the hypothesis named {\ident$_1$} in the local context
+after the hypothesis named {\ident$_2$}.
+
+If {\ident$_1$} comes before {\ident$_2$} in the order of dependences,
+then all hypotheses between {\ident$_1$} and {\ident$_2$} which
+(possibly indirectly) depend on {\ident$_1$} are moved also.
+
+If {\ident$_1$} comes after {\ident$_2$} in the order of dependences,
+then all hypotheses between {\ident$_1$} and {\ident$_2$} which 
+(possibly indirectly) occur in {\ident$_1$} are moved also.
+
+\begin{Variants}
+
+\item {\tt move {\ident$_1$} before {\ident$_2$}}
+
+This moves {\ident$_1$} towards and just before the hypothesis named {\ident$_2$}.
+
+\item {\tt move {\ident} at top}
+
+This moves {\ident} at the top of the local context (at the beginning of the context).
+
+\item {\tt move {\ident} at bottom}
+
+This moves {\ident} at the bottom of the local context (at the end of the context).
+
+\end{Variants}
+
+\begin{ErrMsgs}
+
+\item \errindex{{\ident$_i$} not found}
+
+\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
+                   it occurs in {\ident$_2$}}
+
+\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
+                   it depends on {\ident$_2$}}
+
+\end{ErrMsgs}
+
+\subsection{\tt rename {\ident$_1$} into {\ident$_2$}
+\tacindex{rename}}
+
+This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current
+context\footnote{but it does not rename the hypothesis in the
+  proof-term...}
+
+\begin{Variants}
+
+\item {\tt rename {\ident$_1$} into {\ident$_2$}, \ldots,
+    {\ident$_{2k-1}$} into {\ident$_{2k}$}}
+
+ Is equivalent to the sequence of the corresponding atomic {\tt rename}. 
+
+\end{Variants}
+
+\begin{ErrMsgs}
+
+\item \errindex{{\ident$_1$} not found}
+
+\item \errindexbis{{\ident$_2$} is already used}{is already used}
+
+\end{ErrMsgs}
+
+\subsection{\tt intro
+\tacindex{intro}
+\label{intro}}
+
+This tactic applies to a goal which is either a product or starts with
+a let binder. If the goal is a product, the tactic implements the
+``Lam''\index{Typing rules!Lam} rule given in
+Section~\ref{Typed-terms}\footnote{Actually, only the second subgoal will be
+generated since the other one can be automatically checked.}.  If the
+goal starts with a let binder then the tactic implements a mix of the
+``Let''\index{Typing rules!Let} and ``Conv''\index{Typing rules!Conv}.
+
+If the current goal is a dependent product {\tt forall $x$:$T$, $U$} (resp {\tt
+let $x$:=$t$ in $U$}) then {\tt intro} puts {\tt $x$:$T$} (resp {\tt $x$:=$t$})
+ in the local context.
+% Obsolete (quantified names already avoid hypotheses names):
+% Otherwise, it puts
+% {\tt x}{\it n}{\tt :T} where {\it n} is such that {\tt x}{\it n} is a
+%fresh name.
+The new subgoal is $U$.
+% If the {\tt x} has been renamed {\tt x}{\it n} then it is replaced 
+% by {\tt x}{\it n} in {\tt U}. 
+
+If the goal is a non dependent product {\tt $T$ -> $U$}, then it puts
+in the local context either {\tt H}{\it n}{\tt :$T$} (if $T$ is of
+type {\tt Set} or {\tt Prop}) or {\tt X}{\it n}{\tt :$T$} (if the type
+of $T$ is {\tt Type}). The optional index {\it n} is such that {\tt
+H}{\it n} or {\tt X}{\it n} is a fresh identifier.
+In both cases the new subgoal is $U$.
+
+If the goal is neither a product nor starting with a let definition,
+the tactic {\tt intro} applies the tactic {\tt red} until the tactic
+{\tt intro} can be applied or the goal is not reducible.
+
+\begin{ErrMsgs}
+\item \errindex{No product even after head-reduction}
+\item \errindexbis{{\ident} is already used}{is already used}
+\end{ErrMsgs}
+
+\begin{Variants}
+
+\item {\tt intros}\tacindex{intros}
+
+  Repeats {\tt intro} until it meets the head-constant. It never reduces
+  head-constants and it never fails.
+
+\item {\tt intro {\ident}}
+
+  Applies {\tt intro} but forces {\ident} to be the name of the
+  introduced hypothesis.
+
+  \ErrMsg \errindex{name {\ident} is already used}
+
+  \Rem If a name used by {\tt intro} hides the base name of a global
+  constant then the latter can still be referred to by a qualified name
+  (see \ref{LongNames}).
+
+\item {\tt intros \ident$_1$ \dots\ \ident$_n$} 
+  
+  Is equivalent to the composed tactic {\tt intro \ident$_1$; \dots\ ;
+    intro \ident$_n$}.
+
+  More generally, the \texttt{intros} tactic takes a pattern as
+  argument in order to introduce names for components of an inductive
+  definition or to clear introduced hypotheses; This is explained
+  in~\ref{intros-pattern}.
+
+\item {\tt intros until {\ident}} \tacindex{intros until}
+  
+  Repeats {\tt intro} until it meets a premise of the goal having form
+  {\tt (} {\ident}~{\tt :}~{\term} {\tt )} and discharges the variable
+  named {\ident} of the current goal.
+
+  \ErrMsg \errindex{No such hypothesis in current goal}
+  
+\item {\tt intros until {\num}}  \tacindex{intros until}
+  
+  Repeats {\tt intro} until the {\num}-th non-dependent product. For
+  instance, on the subgoal % 
+  \verb+forall x y:nat, x=y -> y=x+ the tactic \texttt{intros until 1}
+  is equivalent to \texttt{intros x y H}, as \verb+x=y -> y=x+ is the
+  first non-dependent product. And on the subgoal %
+  \verb+forall x y z:nat, x=y -> y=x+ the tactic \texttt{intros until 1}
+  is equivalent to \texttt{intros x y z} as the product on \texttt{z}
+  can be rewritten as a non-dependent product: %
+  \verb+forall x y:nat, nat -> x=y -> y=x+
+
+
+  \ErrMsg \errindex{No such hypothesis in current goal}
+
+  Happens when {\num} is 0 or is greater than the number of non-dependent
+  products of the goal.
+
+\item {\tt intro after \ident} \tacindex{intro after}\\
+      {\tt intro before \ident} \tacindex{intro before}\\
+      {\tt intro at top} \tacindex{intro at top}\\
+      {\tt intro at bottom} \tacindex{intro at bottom}
+
+  Applies {\tt intro} and moves the freshly introduced hypothesis
+  respectively after the hypothesis \ident{}, before the hypothesis
+  \ident{}, at the top of the local context, or at the bottom of the
+  local context. All hypotheses on which the new hypothesis depends
+  are moved too so as to respect the order of dependencies between
+  hypotheses. Note that {\tt intro at bottom} is a synonym for {\tt
+  intro} with no argument.
+
+\begin{ErrMsgs}
+\item \errindex{No product even after head-reduction}
+\item \errindex{No such hypothesis} : {\ident}
+\end{ErrMsgs}
+
+\item {\tt intro \ident$_1$ after \ident$_2$}\\
+      {\tt intro \ident$_1$ before \ident$_2$}\\
+      {\tt intro \ident$_1$ at top}\\
+      {\tt intro \ident$_1$ at bottom}
+  
+  Behaves as previously but naming the introduced hypothesis
+  \ident$_1$.  It is equivalent to {\tt intro \ident$_1$} followed by
+  the appropriate call to {\tt move}~(see Section~\ref{move}).
+
+\begin{ErrMsgs}
+\item \errindex{No product even after head-reduction}
+\item \errindex{No such hypothesis} : {\ident}
+\end{ErrMsgs}
+
+\end{Variants}
+
+\subsection{\tt apply \term
+\tacindex{apply}
+\label{apply}}
+
+This tactic applies to any goal.  The argument {\term} is a term
+well-formed in the local context.  The tactic {\tt apply} tries to
+match the current goal against the conclusion of the type of {\term}.
+If it succeeds, then the tactic returns as many subgoals as the number
+of non dependent premises of the type of {\term}. If the conclusion of
+the type of {\term} does not match the goal {\em and} the conclusion
+is an inductive type isomorphic to a tuple type, then each component
+of the tuple is recursively matched to the goal in the left-to-right
+order.
+
+The tactic {\tt apply} relies on first-order unification with
+dependent types unless the conclusion of the type of {\term} is of the
+form {\tt ($P$~ $t_1$~\ldots ~$t_n$)} with $P$ to be instantiated.  In
+the latter case, the behavior depends on the form of the goal. If the
+goal is of the form {\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$} and the
+$t_i$ and $u_i$ unifies, then $P$ is taken to be (fun $x$ => $Q$).
+Otherwise, {\tt apply} tries to define $P$ by abstracting over
+$t_1$~\ldots ~$t_n$ in the goal. See {\tt pattern} in
+Section~\ref{pattern} to transform the goal so that it gets the form
+{\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$}.
+
+\begin{ErrMsgs}
+\item \errindex{Impossible to unify \dots\ with \dots} 
+
+  The {\tt apply}
+  tactic failed to match the conclusion of {\term} and the current goal.
+  You can help the {\tt apply} tactic by transforming your
+  goal with the {\tt change} or {\tt pattern} tactics (see 
+  sections~\ref{pattern},~\ref{change}).
+
+\item \errindex{Unable to find an instance for the variables
+{\ident} \ldots {\ident}}
+
+  This occurs when some instantiations of the premises of {\term} are not
+  deducible from the unification. This is the case, for instance, when
+  you want to apply a transitivity property. In this case, you have to
+  use one of the variants below:
+
+\end{ErrMsgs}
+
+\begin{Variants}
+
+\item{\tt apply {\term} with {\term$_1$} \dots\ {\term$_n$}} 
+  \tacindex{apply \dots\ with}
+  
+  Provides {\tt apply} with explicit instantiations for all dependent
+  premises of the type of {\term} which do not occur in the conclusion
+  and consequently cannot be found by unification. Notice that
+  {\term$_1$} \dots\ {\term$_n$} must be given according to the order
+  of these dependent premises of the type of {\term}.
+
+  \ErrMsg \errindex{Not the right number of missing arguments}
+
+\item{\tt apply {\term} with ({\vref$_1$} := {\term$_1$}) \dots\ ({\vref$_n$}
+    := {\term$_n$})} 
+  
+  This also provides {\tt apply} with values for instantiating
+  premises. Here, variables are referred by names and non-dependent
+  products by increasing numbers (see syntax in Section~\ref{Binding-list}).
+
+\item {\tt apply} {\term$_1$} {\tt ,} \ldots {\tt ,} {\term$_n$} 
+
+  This is a shortcut for {\tt apply} {\term$_1$} {\tt ; [ ..~|}
+   \ldots~{\tt ; [ ..~| {\tt apply} {\term$_n$} ]} \ldots~{\tt ]}, i.e. for the
+   successive applications of {\term$_{i+1}$} on the last subgoal
+   generated by {\tt apply} {\term$_i$}, starting from the application
+   of {\term$_1$}.
+
+\item {\tt eapply \term}\tacindex{eapply}\label{eapply}
+  
+  The tactic {\tt eapply} behaves as {\tt apply} but does not fail
+  when no instantiation are deducible for some variables in the
+  premises.  Rather, it turns these variables into so-called
+  existential variables which are variables still to instantiate. An
+  existential variable is identified by a name of the form {\tt ?$n$}
+  where $n$ is a number.  The instantiation is intended to be found
+  later in the proof.
+
+  An example of use of {\tt eapply} is given in
+  Section~\ref{eapply-example}. 
+
+\item {\tt simple apply {\term}} \tacindex{simple apply} 
+
+  This behaves like {\tt apply} but it reasons modulo conversion only
+  on subterms that contain no variables to instantiate. For instance,
+  if {\tt id := fun x:nat => x} and {\tt H : forall y, id y = y} then
+  {\tt simple apply H} on goal {\tt O = O} does not succeed because it
+  would require the conversion of {\tt f ?y} and {\tt O} where {\tt
+  ?y} is a variable to instantiate. Tactic {\tt simple apply} does not
+  either traverse tuples as {\tt apply} does.
+
+  Because it reasons modulo a limited amount of conversion, {\tt
+  simple apply} fails quicker than {\tt apply} and it is then
+  well-suited for uses in used-defined tactics that backtrack often.
+
+\item \zeroone{{\tt simple}} {\tt apply} {\term$_1$} \zeroone{{\tt with}
+  {\bindinglist$_1$}} {\tt ,} \ldots {\tt ,} {\term$_n$} \zeroone{{\tt with}
+  {\bindinglist$_n$}}\\
+  \zeroone{{\tt simple}} {\tt eapply} {\term$_1$} \zeroone{{\tt with}
+  {\bindinglist$_1$}} {\tt ,} \ldots {\tt ,} {\term$_n$} \zeroone{{\tt with}
+  {\bindinglist$_n$}}
+
+  This summarizes the different syntaxes for {\tt apply}.
+
+\item {\tt lapply {\term}} \tacindex{lapply} 
+
+  This tactic applies to any goal, say {\tt G}.  The argument {\term}
+  has to be well-formed in the current context, its type being
+  reducible to a non-dependent product {\tt A -> B} with {\tt B}
+  possibly containing products. Then it generates two subgoals {\tt
+  B->G} and {\tt A}. Applying {\tt lapply H} (where {\tt H} has type
+  {\tt A->B} and {\tt B} does not start with a product) does the same
+  as giving the sequence {\tt cut B. 2:apply H.} where {\tt cut} is
+  described below.
+
+  \Warning When {\term} contains more than one non
+  dependent product the tactic {\tt lapply} only takes into account the
+  first product.
+
+\end{Variants}
+
+\subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )}
+\label{tactic:set}
+\tacindex{set}
+\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
+{\tt :=} \term} to the local context. The default is to make this
+replacement only in the conclusion.
+
+\begin{Variants}
+
+\item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occgoalset}}
+
+This notation allows to specify which occurrences of {\term} have to
+be substituted in the context. The {\tt in {\occgoalset}} 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 } {\term}
+
+  This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident}
+  is generated by {\Coq}. This variant also supports an occurrence clause.
+
+\item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term}
+      {\tt ) in {\occgoalset}}\\
+      {\tt set {\term} in {\occgoalset}}
+
+  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 {\occgoalset}}
+
+  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. It is equivalent to {\tt set ( {\ident} {\tt :=}
+  {\term} {\tt ) in |-}}.
+
+\item {\tt pose (} {\ident} \nelist{\binder}{} {\tt :=} {\term} {\tt )}
+
+  This is equivalent to {\tt pose (} {\ident} {\tt :=} {\tt fun}
+  \nelist{\binder}{} {\tt =>} {\term} {\tt )}.
+
+\item{\tt pose {\term}}
+
+  This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but
+  {\ident} is generated by {\Coq}.
+
+\end{Variants}
+
+\subsection{{\tt assert ( {\ident} : {\form} \tt )}
+\tacindex{assert}}
+
+This tactic applies to any goal. {\tt assert (H : U)} adds a new
+hypothesis of name \texttt{H} asserting \texttt{U} to the current goal
+and opens a new subgoal \texttt{U}\footnote{This corresponds to the
+  cut rule of sequent calculus.}. The subgoal {\texttt U} comes first
+in the list of subgoals remaining to prove.
+
+\begin{ErrMsgs}
+\item \errindex{Not a proposition or a type}
+  
+  Arises when the argument {\form} is neither of type {\tt Prop}, {\tt
+    Set} nor {\tt Type}.
+
+\end{ErrMsgs}
+
+\begin{Variants}
+
+\item{\tt assert {\form}}
+  
+  This behaves as {\tt assert (} {\ident} : {\form} {\tt )} but
+  {\ident} is generated by {\Coq}.
+
+\item{\tt assert (} {\ident} := {\term} {\tt )}
+  
+  This behaves as {\tt assert ({\ident} : {\type});[exact
+    {\term}|idtac]} where {\type} is the type of {\term}.
+
+\item {\tt cut {\form}}\tacindex{cut} 
+  
+  This tactic applies to any goal. It implements the non dependent
+  case of the ``App''\index{Typing rules!App} rule given in
+  Section~\ref{Typed-terms}. (This is Modus Ponens inference rule.)
+  {\tt cut U} transforms the current goal \texttt{T} into the two
+  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 applies {\tac}
+  to solve the subgoals generated by \texttt{assert}.
+
+\item \texttt{assert {\form} as {\intropattern}\tacindex{assert as}}
+
+  If {\intropattern} is a naming introduction pattern (see
+  Section~\ref{intros-pattern}), the hypothesis is named after this
+  introduction pattern (in particular, if {\intropattern} is {\ident},
+  the tactic behaves like \texttt{assert ({\ident} : {\form})}).
+
+  If {\intropattern} is a disjunctive/conjunctive introduction
+  pattern, the tactic behaves like \texttt{assert {\form}} then destructing the
+  resulting hypothesis using the given introduction pattern.
+
+\item \texttt{assert {\form} as {\intropattern} by {\tac}}
+
+  This combines the two previous variants of {\tt assert}.
+
+\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}}
+
+  This tactic behaves like \texttt{assert T as {\intropattern} by
+  exact {\term}} where \texttt{T} is the type of {\term}.
+
+  In particular, \texttt{pose proof {\term} as {\ident}} behaves as
+  \texttt{assert ({\ident}:T) by exact {\term}} (where \texttt{T} is
+  the type of {\term}) and \texttt{pose proof {\term} as
+  {\disjconjintropattern}\tacindex{pose proof}} behaves
+  like \texttt{destruct {\term} as {\disjconjintropattern}}.
+
+\item {\tt specialize ({\ident} \term$_1$ {\ldots} \term$_n$)\tacindex{specialize}} \\
+      {\tt specialize {\ident} with \bindinglist}
+
+      The tactic {\tt specialize} works on local hypothesis \ident.
+      The premises of this hypothesis (either universal
+      quantifications or non-dependent implications) are instantiated
+      by concrete terms coming either from arguments \term$_1$
+      $\ldots$ \term$_n$ or from a bindings list (see
+      Section~\ref{Binding-list} for more about bindings lists). In the
+      second form, all instantiation elements must be given, whereas
+      in the first form the application to \term$_1$ {\ldots}
+      \term$_n$ can be partial. The first form is equivalent to 
+      {\tt assert (\ident':=\ident \term$_1$ {\ldots} \term$_n$);
+           clear \ident; rename \ident' into \ident}. 
+
+      The name {\ident} can also refer to a global lemma or
+      hypothesis. In this case, for compatibility reasons, the
+      behavior of {\tt specialize} is close to that of {\tt
+        generalize}: the instantiated statement becomes an additional 
+      premise of the goal. 
+
+%% Moreover, the old syntax allows the use of a number after {\tt specialize} 
+%% for controlling the number of premises to instantiate. Giving this 
+%% number should not be mandatory anymore (automatic detection of how
+%% many premises can be eaten without leaving meta-variables). Hence 
+%% no documentation for this integer optional argument of specialize
+
+\end{Variants}
+
+\subsection{{\tt apply {\term} in {\ident}}
+\tacindex{apply \ldots\ in}}
+
+This tactic applies to any goal.  The argument {\term} is a term
+well-formed in the local context and the argument {\ident} is an
+hypothesis of the context.  The tactic {\tt apply {\term} in {\ident}}
+tries to match the conclusion of the type of {\ident} against a non
+dependent premise of the type of {\term}, trying them from right to
+left.  If it succeeds, the statement of hypothesis {\ident} is
+replaced by the conclusion of the type of {\term}. The tactic also
+returns as many subgoals as the number of other non dependent premises
+in the type of {\term} and of the non dependent premises of the type
+of {\ident}.  If the conclusion of the type of {\term} does not match
+the goal {\em and} the conclusion is an inductive type isomorphic to a
+tuple type, then the tuple is (recursively) decomposed and the first
+component of the tuple of which a non dependent premise matches the
+conclusion of the type of {\ident}. Tuples are decomposed in a
+width-first left-to-right order (for instance if the type of {\tt H1}
+is a \verb=A <-> B= statement, and the type of {\tt H2} is \verb=A=
+then {\tt apply H1 in H2} transforms the type of {\tt H2} into {\tt
+  B}). The tactic {\tt apply} relies on first-order pattern-matching
+with dependent types.
+
+\begin{ErrMsgs}
+\item \errindex{Statement without assumptions}
+
+This happens if the type of {\term} has no non dependent premise.
+
+\item \errindex{Unable to apply}
+
+This happens if the conclusion of {\ident} does not match any of the
+non dependent premises of the type of {\term}.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt apply \nelist{\term}{,} in {\ident}}
+
+This applies each of {\term} in sequence in {\ident}.
+
+\item {\tt apply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
+
+This does the same but uses the bindings in each {\bindinglist} to 
+instantiate the parameters of the corresponding type of {\term}
+(see syntax of bindings in Section~\ref{Binding-list}).
+
+\item {\tt eapply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
+\tacindex{eapply {\ldots} in}
+
+This works as {\tt apply \nelist{{\term} {\bindinglist}}{,} in
+{\ident}} but turns unresolved bindings into existential variables, if
+any, instead of failing.
+
+\item {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in
+{\ident}} then destructs the hypothesis {\ident} along
+{\disjconjintropattern} as {\tt destruct {\ident} as
+{\disjconjintropattern}} would.
+
+\item {\tt eapply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
+
+\item {\tt simple apply {\term} in {\ident}}
+\tacindex{simple apply {\ldots} in} 
+\tacindex{simple eapply {\ldots} in} 
+
+This behaves like {\tt apply {\term} in {\ident}} but it reasons
+modulo conversion only on subterms that contain no variables to
+instantiate. For instance, if {\tt id := fun x:nat => x} and {\tt H :
+  forall y, id y = y -> True} and {\tt H0 : O = O} then {\tt simple
+  apply H in H0} does not succeed because it would require the
+conversion of {\tt f ?y} and {\tt O} where {\tt ?y} is a variable to
+instantiate.  Tactic {\tt simple apply {\term} in {\ident}} does not
+either traverse tuples as {\tt apply {\term} in {\ident}} does.
+
+\item {\tt simple apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}\\
+{\tt simple eapply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This are the general forms of {\tt simple apply {\term} in {\ident}} and 
+{\tt simple eapply {\term} in {\ident}}.
+\end{Variants}
+
+\subsection{\tt generalize \term
+\tacindex{generalize}
+\label{generalize}}
+
+This tactic applies to any goal. It generalizes the conclusion w.r.t.
+one subterm of it. For example:
+
+\begin{coq_eval}
+Goal forall x y:nat, (0 <= x + y + y).
+intros.
+\end{coq_eval}
+\begin{coq_example}
+Show.
+generalize (x + y + y).
+\end{coq_example}
+
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+If the goal is $G$ and $t$ is a subterm of type $T$ in the goal, then
+{\tt generalize} \textit{t} replaces the goal by {\tt forall (x:$T$), $G'$}
+where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by
+{\tt x}. The name of the variable (here {\tt n}) is chosen based on $T$.
+
+\begin{Variants}
+\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}
+  
+  This generalizes {\term} but also {\em all} hypotheses which depend
+  on {\term}. It clears the generalized hypotheses.
+
+\end{Variants}
+
+
+\subsection{\tt revert  \ident$_1$ \dots\ \ident$_n$
+\tacindex{revert}
+\label{revert}}
+
+This applies to any goal with variables \ident$_1$ \dots\ \ident$_n$.
+It moves the hypotheses (possibly defined) to the goal, if this respects
+dependencies. This tactic is the inverse of {\tt intro}. 
+
+\begin{ErrMsgs}
+\item \errindexbis{{\ident} is used in the hypothesis {\ident'}}{is
+    used in the hypothesis} 
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt revert dependent \ident \tacindex{revert dependent}}
+
+ This moves to the goal the hypothesis \ident\ and all hypotheses
+ which depend on it.
+
+\end{Variants}
+
+\subsection{\tt change \term
+\tacindex{change}
+\label{change}}
+
+This tactic applies to any goal. It implements the rule
+``Conv''\index{Typing rules!Conv} given in Section~\ref{Conv}.  {\tt
+  change U} replaces the current goal \T\ with \U\ providing that
+\U\ is well-formed and that \T\ and \U\ are convertible.
+
+\begin{ErrMsgs}
+\item \errindex{Not convertible}
+\end{ErrMsgs}
+
+\tacindex{change \dots\ in}
+\begin{Variants}
+\item {\tt change \term$_1$ with \term$_2$} 
+  
+  This replaces the occurrences of \term$_1$ by \term$_2$ in the
+  current goal.  The terms \term$_1$ and \term$_2$ must be
+  convertible.
+
+\item {\tt change \term$_1$ at \num$_1$ \dots\ \num$_i$ with \term$_2$} 
+  
+  This replaces the occurrences numbered \num$_1$ \dots\ \num$_i$ of
+  \term$_1$ by \term$_2$ in the current goal.
+  The terms \term$_1$ and \term$_2$ must be convertible.
+
+  \ErrMsg {\tt Too few occurrences}
+
+\item {\tt change {\term} in {\ident}}
+
+\item {\tt change \term$_1$ with \term$_2$ in {\ident}}
+  
+\item {\tt change \term$_1$ at  \num$_1$ \dots\ \num$_i$ with \term$_2$ in
+    {\ident}}
+  
+  This applies the {\tt change} tactic not to the goal but to the
+  hypothesis {\ident}.
+
+\end{Variants}
+
+\SeeAlso \ref{Conversion-tactics}
+
+\subsection{\tt fix {\ident} {\num}
+\tacindex{fix}
+\label{tactic:fix}}
+
+This tactic is a primitive tactic to start a proof by induction. In
+general, it is easier to rely on higher-level induction tactics such
+as the ones described in Section~\ref{Tac-induction}.
+
+In the syntax of the tactic, the identifier {\ident} is the name given
+to the induction hypothesis. The natural number {\num} tells on which
+premise of the current goal the induction acts, starting
+from 1 and counting both dependent and non dependent
+products. Especially, the current lemma must be composed of at least
+{\num} products.
+
+Like in a {\tt fix} expression, the induction
+hypotheses have to be used on structurally smaller arguments.
+The verification that inductive proof arguments are correct is done
+only at the time of registering the lemma in the environment. To know
+if the use of induction hypotheses is correct at some
+time of the interactive development of a proof, use the command {\tt
+  Guarded} (see Section~\ref{Guarded}).
+
+\begin{Variants}
+  \item {\tt fix} {\ident}$_1$ {\num} {\tt with (} {\ident}$_2$
+    \nelist{{\binder}$_{2}$}{} \zeroone{{\tt \{ struct {\ident$'_2$}
+      \}}} {\tt :} {\type}$_2$ {\tt )} {\ldots} {\tt (} {\ident}$_1$
+    \nelist{{\binder}$_n$}{} \zeroone{{\tt \{ struct {\ident$'_n$} \}}}
+           {\tt :} {\type}$_n$ {\tt )}
+
+This starts a proof by mutual induction. The statements to be
+simultaneously proved are respectively {\tt forall}
+  \nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+  \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$.  The identifiers
+{\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the induction
+hypotheses. The identifiers {\ident}$'_2$ {\ldots} {\ident}$'_n$ are the
+respective names of the premises on which the induction is performed
+in the statements to be simultaneously proved (if not given, the
+system tries to guess itself what they are).
+
+\end{Variants}
+
+\subsection{\tt cofix {\ident}
+\tacindex{cofix}
+\label{tactic:cofix}}
+
+This tactic starts a proof by coinduction. The identifier {\ident} is
+the name given to the coinduction hypothesis.  Like in a {\tt cofix}
+expression, the use of induction hypotheses have to guarded by a
+constructor.  The verification that the use of coinductive hypotheses
+is correct is done only at the time of registering the lemma in the
+environment. To know if the use of coinduction hypotheses is correct
+at some time of the interactive development of a proof, use the
+command {\tt Guarded} (see Section~\ref{Guarded}).
+
+
+\begin{Variants}
+  \item {\tt cofix} {\ident}$_1$ {\tt with (} {\ident}$_2$
+    \nelist{{\binder}$_2$}{} {\tt :} {\type}$_2$ {\tt )} {\ldots} {\tt
+      (} {\ident}$_1$ \nelist{{\binder}$_1$}{} {\tt :} {\type}$_n$
+           {\tt )}
+
+This starts a proof by mutual coinduction. The statements to be
+simultaneously proved are respectively {\tt forall}
+\nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+  \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$. The identifiers
+    {\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the
+    coinduction hypotheses.
+
+\end{Variants}
+
+\subsection{\tt evar (\ident:\term)
+\tacindex{evar}
+\label{evar}}
+
+The {\tt evar} tactic creates a new local definition named \ident\ with
+type \term\ in the context. The body of this binding is a fresh
+existential variable.
+
+\subsection{\tt instantiate (\num:= \term)
+\tacindex{instantiate}
+\label{instantiate}}
+
+The {\tt instantiate} tactic allows to solve an existential variable
+with the term \term. The \num\  argument is the position of the
+existential variable from right to left in the conclusion. This cannot be
+the number of the existential variable since this number is different
+in every session.
+
+\begin{Variants}
+  \item {\tt instantiate (\num:=\term) in \ident}
+  
+  \item {\tt instantiate (\num:=\term) in (Value of \ident)}
+  
+  \item {\tt instantiate (\num:=\term) in (Type of \ident)}
+
+These allow to refer respectively to existential variables occurring in 
+a hypothesis or in the body or the type of a local definition.  
+
+  \item {\tt instantiate}
+
+    Without argument, the {\tt instantiate} tactic tries to solve as
+    many existential variables as possible, using information gathered
+    from other tactics in the same tactical. This is automatically
+    done after each complete tactic (i.e. after a dot in proof mode),
+    but not, for example, between each tactic when they are sequenced
+    by semicolons.
+
+\end{Variants}
+
+\subsection{\tt admit
+\tacindex{admit}
+\label{admit}}
+
+The {\tt admit} tactic ``solves'' the current subgoal by an
+axiom. This typically allows to temporarily skip a subgoal so as to
+progress further in the rest of the proof. To know if some proof still
+relies on unproved subgoals, one can use the command {\tt Print
+Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals
+have names of the form {\ident}\texttt{\_admitted} possibly followed
+by a number.
+
+\subsection{Bindings list
+\index{Binding list}
+\label{Binding-list}}
+
+Tactics that take a term as argument may also support a 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} {\occgoalset} \\
+{\occgoalset} & ::= &
+    \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
+&   & {\dots} {\tt ,}\\
+&   & {\ident$_m$} \zeroone{\atoccurrences}}\\
+&   & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\
+& | &
+    {\tt *} {\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}\\
+& | &
+    {\tt *}\\
+{\atoccurrences} & ::= & {\tt at} {\occlist}\\
+{\occlist} & ::= & \zeroone{{\tt -}} {\num$_1$} \dots\ {\num$_n$}
+\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.
+
+If a minus sign is given between {\tt at} and the list of occurrences,
+it negates the condition so that the clause denotes all the occurrences except
+the ones explicitly mentioned after the minus sign.
+
+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
+\tacindex{absurd}
+\label{absurd}}
+
+This tactic applies to any goal. The argument {\term} is any
+proposition {\tt P} of type {\tt Prop}. This tactic applies {\tt
+  False} elimination, that is it deduces the current goal from {\tt
+  False}, and generates as subgoals {\tt $\sim$P} and {\tt P}. It is
+very useful in proofs by cases, where some cases are impossible. In
+most cases, \texttt{P} or $\sim$\texttt{P} is one of the hypotheses of
+the local context.
+
+\subsection{\tt contradiction
+\label{contradiction}
+\tacindex{contradiction}}
+
+This tactic applies to any goal. The {\tt contradiction} tactic
+attempts to find in the current context (after all {\tt intros}) one
+hypothesis which is equivalent to {\tt False}. It permits to prune 
+irrelevant cases. This tactic is a macro for the tactics sequence 
+{\tt intros; elimtype False; assumption}. 
+
+\begin{ErrMsgs}
+\item \errindex{No such assumption}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt contradiction \ident}
+
+The proof of {\tt False} is searched in the hypothesis named \ident.
+\end{Variants}
+
+\subsection {\tt contradict \ident}
+\label{contradict}
+\tacindex{contradict}
+
+This tactic allows to manipulate negated hypothesis and goals. The
+name \ident\ should correspond to a hypothesis. With 
+{\tt contradict H}, the current goal and context is transformed in
+the following way: 
+\begin{itemize}
+\item  {\tt H:$\neg$A $\vd$  B} \ becomes \ {\tt $\vd$ A}
+\item  {\tt H:$\neg$A $\vd$ $\neg$B} \  becomes \ {\tt H: B $\vd$  A }
+\item  {\tt H: A $\vd$  B} \ becomes \ {\tt $\vd$ $\neg$A}
+\item  {\tt H: A $\vd$ $\neg$B} \ becomes \ {\tt H: B $\vd$ $\neg$A}
+\end{itemize}
+
+\subsection{\tt exfalso}
+\label{exfalso}
+\tacindex{exfalso}
+
+This tactic implements the ``ex falso quodlibet'' logical principle:
+an elimination of {\tt False} is performed on the current goal, and the
+user is then required to prove that {\tt False} is indeed provable in
+the current context. This tactic is a macro for {\tt elimtype False}.
+
+\section{Conversion tactics
+\index{Conversion tactics}
+\label{Conversion-tactics}}
+
+This set of tactics implements different specialized usages of the
+tactic \texttt{change}.
+
+All conversion tactics (including \texttt{change}) can be
+parameterized by the parts of the goal where the conversion can
+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 goal clauses)  and
+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 goal clauses is the following:
+\begin{description}
+\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}~{\ident}$_1$\ldots {\ident}$_n$
+performs the conversion in hypotheses {\ident}$_1$\ldots {\ident}$_n$.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%voir reduction__conv_x : histoires d'univers.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection[{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
+\dots\ \flag$_n$} and {\tt compute}]
+{{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
+\dots\ \flag$_n$} and {\tt compute}
+\tacindex{cbv}
+\tacindex{lazy}
+\tacindex{compute}
+\tacindex{vm\_compute}\label{vmcompute}}
+
+These parameterized reduction tactics apply to any goal and perform
+the normalization of the goal according to the specified flags. In
+correspondence with the kinds of reduction considered in \Coq\, namely
+$\beta$ (reduction of functional application), $\delta$ (unfolding of
+transparent constants, see \ref{Transparent}), $\iota$ (reduction of
+pattern-matching over a constructed term, and unfolding of {\tt fix}
+and {\tt cofix} expressions) and $\zeta$ (contraction of local
+definitions), the flag are either {\tt beta}, {\tt delta}, {\tt iota}
+or {\tt zeta}. The {\tt delta} flag itself can be refined into {\tt
+delta [\qualid$_1$\ldots\qualid$_k$]} or {\tt delta
+-[\qualid$_1$\ldots\qualid$_k$]}, restricting in the first case the
+constants to unfold to the constants listed, and restricting in the
+second case the constant to unfold to all but the ones explicitly
+mentioned. Notice that the {\tt delta} flag does not apply to
+variables bound by a let-in construction inside the term itself (use
+here the {\tt zeta} flag). In any cases, opaque constants are not
+unfolded (see Section~\ref{Opaque}).
+
+The goal may be normalized with two strategies: {\em lazy} ({\tt lazy}
+tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy
+is a call-by-need strategy, with sharing of reductions: the arguments of a
+function call are partially evaluated only when necessary, and if an
+argument is used several times then it is computed only once. This
+reduction is efficient for reducing expressions with dead code. For
+instance, the proofs of a proposition {\tt exists~$x$. $P(x)$} reduce to a
+pair of a witness $t$, and a proof that $t$ satisfies the predicate
+$P$. Most of the time, $t$ may be computed without computing the proof
+of $P(t)$, thanks to the lazy strategy.
+
+The call-by-value strategy is the one used in ML languages: the
+arguments of a function call are evaluated first, using a weak
+reduction (no reduction under the $\lambda$-abstractions). Despite the
+lazy strategy always performs fewer reductions than the call-by-value
+strategy, the latter is generally more efficient for evaluating purely
+computational expressions (i.e. with few dead code).
+
+\begin{Variants}
+\item {\tt compute} \tacindex{compute}\\
+      {\tt cbv}
+  
+  These are synonyms for {\tt cbv beta delta iota zeta}.
+
+\item {\tt lazy}
+  
+  This is a synonym for {\tt lazy beta delta iota zeta}.
+
+\item {\tt compute [\qualid$_1$\ldots\qualid$_k$]}\\
+      {\tt cbv [\qualid$_1$\ldots\qualid$_k$]}
+
+  These are synonyms of {\tt cbv beta delta
+  [\qualid$_1$\ldots\qualid$_k$] iota zeta}.
+  
+\item {\tt compute -[\qualid$_1$\ldots\qualid$_k$]}\\
+      {\tt cbv -[\qualid$_1$\ldots\qualid$_k$]}
+
+  These are synonyms of {\tt cbv beta delta
+  -[\qualid$_1$\ldots\qualid$_k$] iota zeta}.
+
+\item {\tt lazy [\qualid$_1$\ldots\qualid$_k$]}\\
+      {\tt lazy -[\qualid$_1$\ldots\qualid$_k$]}
+
+  These are respectively synonyms of {\tt cbv beta delta
+  [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt cbv beta delta
+  -[\qualid$_1$\ldots\qualid$_k$] 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}
+
+% Obsolete? Anyway not very important message
+%\begin{ErrMsgs}
+%\item \errindex{Delta must be specified before}
+%  
+%  A list of constants appeared before the {\tt delta} flag.
+%\end{ErrMsgs}
+
+
+\subsection{{\tt red}
+\tacindex{red}}
+
+This tactic applies to a goal which has the form {\tt
+  forall (x:T1)\dots(xk:Tk), c t1 \dots\ tn} where {\tt c} is a constant.  If
+{\tt c} is transparent then it replaces {\tt c} with its definition
+(say {\tt t}) and then reduces {\tt (t t1 \dots\ tn)} according to
+$\beta\iota\zeta$-reduction rules.
+
+\begin{ErrMsgs}
+\item \errindex{Not reducible}
+\end{ErrMsgs}
+
+\subsection{{\tt hnf}
+\tacindex{hnf}}
+
+This tactic applies to any goal. It replaces the current goal with its
+head normal form according to the $\beta\delta\iota\zeta$-reduction
+rules, i.e.  it reduces the head of the goal until it becomes a
+product or an irreducible term.
+
+\Example
+The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}.
+
+\Rem The $\delta$ rule only applies to transparent constants
+(see Section~\ref{Opaque} on transparency and opacity).
+
+\subsection{\tt simpl
+\tacindex{simpl}}
+
+This tactic applies to any goal. The tactic {\tt simpl} first applies
+$\beta\iota$-reduction rule.  Then it expands transparent constants
+and tries to reduce {\tt T'} according, once more, to $\beta\iota$
+rules. But when the $\iota$ rule is not applicable then possible
+$\delta$-reductions are not applied.  For instance trying to use {\tt
+simpl} on {\tt (plus n O)=n} changes nothing.  Notice that only
+transparent constants whose name can be reused as such in the
+recursive calls are possibly unfolded. For instance a constant defined
+by {\tt plus' := plus} is possibly unfolded and reused in the
+recursive calls, but a constant such as {\tt succ := plus (S O)} is
+never unfolded.
+
+\tacindex{simpl \dots\ in}
+\begin{Variants}
+\item {\tt simpl {\term}}
+  
+  This applies {\tt simpl} only to the occurrences of {\term} in the
+  current goal.
+
+\item {\tt simpl {\term} at \num$_1$ \dots\ \num$_i$}
+  
+  This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
+  occurrences of {\term} in the current goal.
+
+  \ErrMsg {\tt Too few occurrences}
+
+\item {\tt simpl {\ident}}
+  
+  This applies {\tt simpl} only to the applicative subterms whose head
+  occurrence is {\ident}.
+
+\item {\tt simpl {\ident} at \num$_1$ \dots\ \num$_i$}
+  
+  This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
+applicative subterms whose head occurrence is {\ident}.
+
+\end{Variants}
+
+\subsection{\tt unfold \qualid
+\tacindex{unfold}
+\label{unfold}}
+
+This tactic applies to any goal. The argument {\qualid} must denote a
+defined transparent constant or local definition (see Sections~\ref{Basic-definitions} and~\ref{Transparent}).  The tactic {\tt
+  unfold} applies the $\delta$ rule to each occurrence of the constant
+to which {\qualid} refers in the current goal and then replaces it
+with its $\beta\iota$-normal form.
+
+\begin{ErrMsgs}
+\item {\qualid} \errindex{does not denote an evaluable constant}
+
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt unfold {\qualid}$_1$, \dots, \qualid$_n$}
+  \tacindex{unfold \dots\ in}
+  
+  Replaces {\em simultaneously} {\qualid}$_1$, \dots, {\qualid}$_n$
+  with their definitions and replaces the current goal with its
+  $\beta\iota$ normal form.
+
+\item {\tt unfold {\qualid}$_1$ at \num$_1^1$, \dots, \num$_i^1$,
+\dots,\ \qualid$_n$ at \num$_1^n$ \dots\ \num$_j^n$}
+  
+  The lists \num$_1^1$, \dots, \num$_i^1$ and \num$_1^n$, \dots,
+  \num$_j^n$ specify the occurrences of {\qualid}$_1$, \dots,
+  \qualid$_n$ to be unfolded. Occurrences are located from left to
+  right.
+
+  \ErrMsg {\tt bad occurrence number of {\qualid}$_i$}
+
+  \ErrMsg {\qualid}$_i$ {\tt does not occur}
+
+\item {\tt unfold {\qstring}}
+
+  If {\qstring} denotes the discriminating symbol of a notation (e.g. {\tt
+  "+"}) or an expression defining a notation (e.g. \verb!"_ + _"!), and
+  this notation refers to an unfoldable constant, then the tactic
+  unfolds it.
+
+\item {\tt unfold {\qstring}\%{\delimkey}}
+
+  This is variant of {\tt unfold {\qstring}} where {\qstring} gets its
+  interpretation from the scope bound to the delimiting key
+  {\delimkey} instead of its default interpretation (see
+  Section~\ref{scopechange}).
+
+\item {\tt unfold \qualidorstring$_1$ at \num$_1^1$, \dots, \num$_i^1$,
+\dots,\ \qualidorstring$_n$ at \num$_1^n$ \dots\ \num$_j^n$}
+
+  This is the most general form, where {\qualidorstring} is either a
+  {\qualid} or a {\qstring} referring to a notation.
+
+\end{Variants}
+
+\subsection{{\tt fold} \term
+\tacindex{fold}}
+
+This tactic applies to any goal. The term \term\ is reduced using the {\tt red}
+tactic. Every occurrence of the resulting term in the goal is then
+replaced by \term.
+
+\begin{Variants}
+\item {\tt fold} \term$_1$ \dots\ \term$_n$ 
+  
+  Equivalent to {\tt fold} \term$_1${\tt;}\ldots{\tt; fold} \term$_n$.
+\end{Variants}
+
+\subsection{{\tt pattern {\term}}
+\tacindex{pattern}
+\label{pattern}}
+
+This command applies to any goal. The argument {\term} must be a free
+subterm of the current goal.  The command {\tt pattern} performs
+$\beta$-expansion (the inverse of $\bt$-reduction) of the current goal
+(say \T) by
+\begin{enumerate}
+\item replacing all occurrences of {\term} in {\T} with a fresh variable
+\item abstracting this variable
+\item applying the abstracted goal to {\term}
+\end{enumerate}
+
+For instance, if the current goal $T$ is expressible has $\phi(t)$
+where the notation captures all the instances of $t$ in $\phi(t)$,
+then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt
+x}$)$) $t$}.  This command can be used, for instance, when the tactic
+{\tt apply} fails on matching.
+
+\begin{Variants}
+\item {\tt pattern {\term} at {\num$_1$} \dots\ {\num$_n$}}
+  
+  Only the occurrences {\num$_1$} \dots\ {\num$_n$} of {\term} are
+  considered for $\beta$-expansion. Occurrences are located from left
+  to right.
+
+\item {\tt pattern {\term} at - {\num$_1$} \dots\ {\num$_n$}}
+  
+  All occurrences except the occurrences of indexes {\num$_1$} \dots\
+  {\num$_n$} of {\term} are considered for
+  $\beta$-expansion. Occurrences are located from left to right.
+
+\item {\tt pattern {\term$_1$}, \dots, {\term$_m$}}
+  
+  Starting from a goal $\phi(t_1 \dots\ t_m)$, the tactic
+   {\tt pattern $t_1$, \dots,\ $t_m$} generates the equivalent goal {\tt
+   (fun (x$_1$:$A_1$) \dots\ (x$_m$:$A_m$) => $\phi(${\tt x$_1$\dots\
+   x$_m$}$)$) $t_1$ \dots\ $t_m$}.\\ If $t_i$ occurs in one of the
+   generated types $A_j$ these occurrences will also be considered and
+   possibly abstracted.
+
+\item {\tt pattern {\term$_1$} at {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots,
+    {\term$_m$} at {\num$_1^m$} \dots\ {\num$_{n_m}^m$}}
+  
+  This behaves as above but processing only the occurrences \num$_1^1$,
+  \dots, \num$_i^1$ of \term$_1$, \dots, \num$_1^m$, \dots, \num$_j^m$
+  of \term$_m$ starting from \term$_m$.
+
+\item {\tt pattern} {\term$_1$} \zeroone{{\tt at \zeroone{-}} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}} {\tt ,} \dots {\tt ,}
+    {\term$_m$} \zeroone{{\tt at \zeroone{-}} {\num$_1^m$} \dots\ {\num$_{n_m}^m$}}
+  
+  This is the most general syntax that combines the different variants.
+
+\end{Variants}
+
+\subsection{Conversion tactics applied to hypotheses}
+
+{\convtactic} {\tt in} \ident$_1$ \dots\ \ident$_n$ 
+
+Applies the conversion tactic {\convtactic} to the
+hypotheses \ident$_1$, \ldots, \ident$_n$. The tactic {\convtactic} is
+any of the conversion tactics listed in this section. 
+
+If \ident$_i$ is a local definition, then \ident$_i$ can be replaced
+by (Type of \ident$_i$) to address not the body but the type of the
+local definition. Example: {\tt unfold not in (Type of H1) (Type of H3).}
+
+\begin{ErrMsgs}
+\item \errindex{No such hypothesis} : {\ident}.
+\end{ErrMsgs}
+
+
+\section{Introductions}
+
+Introduction tactics address goals which are inductive constants.
+They are used when one guesses that the goal can be obtained with one
+of its constructors' type.
+
+\subsection{\tt constructor \num
+\label{constructor}
+\tacindex{constructor}}
+
+This tactic applies to a goal such that the head of its conclusion is
+an inductive constant (say {\tt I}).  The argument {\num} must be less
+or equal to the numbers of constructor(s) of {\tt I}. Let {\tt ci} be
+the {\tt i}-th constructor of {\tt I}, then {\tt constructor i} is
+equivalent to {\tt intros; apply ci}.
+
+\begin{ErrMsgs}
+\item \errindex{Not an inductive product}
+\item \errindex{Not enough constructors}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item \texttt{constructor} 
+  
+  This tries \texttt{constructor 1} then \texttt{constructor 2},
+  \dots\ , then \texttt{constructor} \textit{n} where \textit{n} if
+  the number of constructors of the head of the goal.
+
+\item {\tt constructor \num~with} {\bindinglist}
+  
+  Let {\tt ci} be the {\tt i}-th constructor of {\tt I}, then {\tt
+    constructor i with \bindinglist} is equivalent to {\tt intros;
+    apply ci with \bindinglist}.
+
+  \Warning the terms in the \bindinglist\ are checked
+  in the context where {\tt constructor} is executed and not in the
+  context where {\tt apply} is executed (the introductions are not
+  taken into account).
+
+% To document?
+% \item {\tt constructor {\tactic}}
+
+\item {\tt split}\tacindex{split}
+
+  Applies if {\tt I} has only one constructor, typically in the case
+  of conjunction $A\land B$. Then, it is equivalent to {\tt constructor 1}.
+
+\item {\tt exists {\bindinglist}}\tacindex{exists} 
+
+  Applies if {\tt I} has only one constructor, for instance in the
+  case of existential quantification $\exists x\cdot P(x)$. 
+  Then, it is equivalent to {\tt intros; constructor 1 with \bindinglist}.
+
+\item {\tt exists \nelist{\bindinglist}{,}}
+
+  This iteratively applies {\tt exists {\bindinglist}}.
+
+\item {\tt left}\tacindex{left}\\
+      {\tt right}\tacindex{right}
+
+  Apply if {\tt I} has two constructors, for instance in the case of
+  disjunction $A\lor B$. Then, they are respectively equivalent to {\tt
+    constructor 1} and {\tt constructor 2}.
+  
+\item {\tt left \bindinglist}\\
+      {\tt right \bindinglist}\\
+      {\tt split \bindinglist}
+  
+  As soon as the inductive type has the right number of constructors,
+    these expressions are equivalent to the corresponding {\tt
+    constructor $i$ with \bindinglist}.
+
+\item \texttt{econstructor}\tacindex{econstructor}\\
+      \texttt{eexists}\tacindex{eexists}\\
+      \texttt{esplit}\tacindex{esplit}\\
+      \texttt{eleft}\tacindex{eleft}\\
+      \texttt{eright}\tacindex{eright}\\
+
+  These tactics and their variants behave like \texttt{constructor},
+  \texttt{exists}, \texttt{split}, \texttt{left}, \texttt{right} and
+  their variants but they introduce existential variables instead of
+  failing when the instantiation of a variable cannot be found (cf
+  \texttt{eapply} and Section~\ref{eapply-example}).
+
+\end{Variants}
+
+\section[Induction and Case Analysis]{Induction and Case Analysis
+\label{Tac-induction}}
+
+The tactics presented in this section implement induction or case
+analysis on inductive or coinductive objects (see
+Section~\ref{Cic-inductive-definitions}).
+
+\subsection{\tt induction \term
+\tacindex{induction}}
+
+This tactic applies to any goal. The type of the argument {\term} must
+be an inductive constant. Then, the tactic {\tt induction}
+generates subgoals, one for each possible form of {\term}, i.e. one
+for each constructor of the inductive type.
+
+The tactic {\tt induction} automatically replaces every occurrences
+of {\term} in the conclusion and the hypotheses of the goal.  It
+automatically adds induction hypotheses (using names of the form {\tt
+  IHn1}) to the local context. If some hypothesis must not be taken
+into account in the induction hypothesis, then it needs to be removed
+first (you can also use the tactics {\tt elim} or {\tt simple induction},
+see below).
+
+There are particular cases:
+
+\begin{itemize}
+
+\item If {\term} is an identifier {\ident} denoting a quantified
+variable of the conclusion of the goal, then {\tt induction {\ident}}
+behaves as {\tt intros until {\ident}; induction {\ident}}.
+
+\item If {\term} is a {\num}, then {\tt induction {\num}} behaves as
+{\tt intros until {\num}} followed by {\tt induction} applied to the
+last introduced hypothesis.
+
+\Rem For simple induction on a numeral, use syntax {\tt induction
+({\num})} (not very interesting anyway).
+
+\end{itemize}
+
+\Example
+
+\begin{coq_example}
+Lemma induction_test : forall n:nat, n = n -> n <= n.
+intros n H.
+induction n.
+\end{coq_example}
+
+\begin{ErrMsgs}
+\item \errindex{Not an inductive product}
+\item \errindex{Unable to find an instance for the variables
+{\ident} \ldots {\ident}}
+  
+  Use in this case 
+  the variant {\tt elim \dots\ with \dots} below.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item{\tt induction {\term} as {\disjconjintropattern}}
+  
+  This behaves as {\tt induction {\term}} but uses the names in
+  {\disjconjintropattern} to name the variables introduced in the context.
+  The {\disjconjintropattern} must typically be of the form
+  {\tt [} $p_{11}$ \ldots
+  $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
+    ]} with $m$ being the number of constructors of the type of
+  {\term}. Each variable introduced by {\tt induction} in the context
+  of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
+  $p_{in_i}$ in order. If there are not enough names, {\tt induction}
+  invents names for the remaining variables to introduce. More
+  generally, the $p_{ij}$ can be any disjunctive/conjunctive
+  introduction pattern (see Section~\ref{intros-pattern}). For instance,
+  for an inductive type with one constructor, the pattern notation
+  {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
+  {\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
+
+\item{\tt induction {\term} as {\namingintropattern}}
+
+  This behaves as {\tt induction {\term}} but adds an equation between
+  {\term} and the value that {\term} takes in each of the induction
+  case.  The name of the equation is built according to
+  {\namingintropattern} which can be an identifier, a ``?'', etc, as
+  indicated in Section~\ref{intros-pattern}.
+
+\item{\tt induction {\term} as {\namingintropattern} {\disjconjintropattern}}
+
+  This combines the two previous forms.
+
+\item{\tt induction {\term} with \bindinglist}
+
+  This behaves like \texttt{induction {\term}} providing explicit
+  instances for the premises of the type of {\term} (see the syntax of
+  bindings in Section~\ref{Binding-list}).
+
+\item{\tt einduction {\term}\tacindex{einduction}}
+
+  This tactic behaves like \texttt{induction {\term}} excepts that it
+  does not fail if some dependent premise of the type of {\term} is
+  not inferable. Instead, the unresolved premises are posed as
+  existential variables to be inferred later, in the same way as {\tt
+  eapply} does (see Section~\ref{eapply-example}).
+
+\item {\tt induction {\term$_1$} using {\term$_2$}}
+
+  This behaves as {\tt induction {\term$_1$}} but using {\term$_2$} as
+  induction scheme. It does not expect the conclusion of the type of
+  {\term$_1$} to be inductive.
+
+\item {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}}
+
+  This behaves as {\tt induction {\term$_1$} using {\term$_2$}} but
+  also providing instances for the premises of the type of {\term$_2$}.
+
+\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}}
+
+  This syntax is used for the case {\qualid} denotes an induction principle
+  with complex predicates as the induction principles generated by
+  {\tt Function} or {\tt Functional Scheme} may be.
+
+\item \texttt{induction {\term} in {\occgoalset}}
+
+  This syntax is used for selecting which occurrences of {\term} the
+  induction has to be carried on. The {\tt in {\atoccurrences}} 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 case of the induction is added to the
+  context of the subgoals corresponding to the induction cases (even
+  if no clause {\tt as {\namingintropattern}} is given).
+
+\item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+     {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\namingintropattern} {\disjconjintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+
+  These are the most general forms 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}
+  
+  This is a more basic induction tactic.  Again, the type of the
+  argument {\term} must be an inductive type. Then, according to
+  the type of the goal, the tactic {\tt elim} chooses the appropriate
+  destructor and applies it as the tactic {\tt apply}
+  would do. For instance, if the proof context contains {\tt
+  n:nat} and the current goal is {\tt T} of type {\tt
+  Prop}, then {\tt elim n} is equivalent to {\tt apply nat\_ind with
+  (n:=n)}.  The tactic {\tt elim} does not modify the context of
+  the goal, neither introduces the induction loading into the context
+  of hypotheses.
+
+  More generally, {\tt elim \term} also works when the type of {\term}
+  is a statement with premises and whose conclusion is inductive.  In
+  that case the tactic performs induction on the conclusion of the
+  type of {\term} and leaves the non-dependent premises of the type as
+  subgoals.  In the case of dependent products, the tactic tries to
+  find an instance for which the elimination lemma applies and fails
+  otherwise.
+
+\item {\tt elim {\term} with {\bindinglist}}
+  
+  Allows to give explicit instances to the premises of the type
+  of {\term} (see Section~\ref{Binding-list}).
+
+\item{\tt eelim {\term}\tacindex{eelim}}
+
+  In case the type of {\term} has dependent premises, this turns them into
+  existential variables to be resolved later on.
+
+\item{\tt elim {\term$_1$} using {\term$_2$}}\\
+     {\tt elim {\term$_1$} using {\term$_2$} with {\bindinglist}\tacindex{elim \dots\ using}}
+
+Allows the user to give explicitly an elimination predicate
+{\term$_2$} which is not the standard one for the underlying inductive
+type of {\term$_1$}. The {\bindinglist} clause allows to
+instantiate premises of the type of {\term$_2$}.
+
+\item{\tt elim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}}\\
+     {\tt eelim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}}
+
+  These are the most general forms of {\tt elim} and {\tt eelim}.  It
+  combines the effects of the {\tt using} clause and of the two uses
+  of the {\tt with} clause.
+
+\item {\tt elimtype \form}\tacindex{elimtype}
+  
+  The argument {\form} must be inductively defined. {\tt elimtype I}
+  is equivalent to {\tt cut I. intro H{\rm\sl n}; elim H{\rm\sl n};
+    clear H{\rm\sl n}}. Therefore the hypothesis {\tt H{\rm\sl n}} will
+  not appear in the context(s) of the subgoal(s).  Conversely, if {\tt
+    t} is a term of (inductive) type {\tt I} and which does not occur
+  in the goal then {\tt elim t} is equivalent to {\tt elimtype I; 2:
+    exact t.}
+
+\item {\tt simple induction \ident}\tacindex{simple induction}
+  
+  This tactic behaves as {\tt intros until
+    {\ident}; elim {\tt {\ident}}} when {\ident} is a quantified
+  variable of the goal.
+
+\item {\tt simple induction {\num}}
+  
+  This tactic behaves as {\tt intros until
+    {\num}; elim {\tt {\ident}}} where {\ident} is the name given by
+  {\tt intros until {\num}} to the {\num}-th non-dependent premise of
+  the goal.
+
+%% \item {\tt simple induction {\term}}\tacindex{simple induction}
+  
+%%   If {\term} is an {\ident} corresponding to a quantified variable of
+%%   the goal then the tactic behaves as {\tt intros until {\ident}; elim
+%%   {\tt {\ident}}}.  If {\term} is a {\num} then the tactic behaves as
+%%   {\tt intros until {\ident}; elim {\tt {\ident}}}.  Otherwise, it is
+%%   a synonym for {\tt elim {\term}}.
+
+%%   \Rem For simple induction on a numeral, use syntax {\tt simple
+%%   induction ({\num})}.
+
+\end{Variants}
+
+\subsection{\tt destruct \term
+\tacindex{destruct}}
+\label{destruct}
+
+The tactic {\tt destruct} is used to perform case analysis without
+recursion. Its behavior is similar to {\tt induction} except
+that no induction hypothesis is generated.  It applies to any goal and
+the type of {\term} must be inductively defined. There are particular cases:
+
+\begin{itemize}
+
+\item If {\term} is an identifier {\ident} denoting a quantified
+variable of the conclusion of the goal, then {\tt destruct {\ident}}
+behaves as {\tt intros until {\ident}; destruct {\ident}}.
+
+\item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as
+{\tt intros until {\num}} followed by {\tt destruct} applied to the
+last introduced hypothesis.
+
+\Rem For destruction of a numeral, use syntax {\tt destruct
+({\num})} (not very interesting anyway).
+
+\end{itemize}
+
+\begin{Variants}
+\item{\tt destruct {\term} as {\disjconjintropattern}}
+  
+  This behaves as {\tt destruct {\term}} but uses the names in
+  {\intropattern} to name the variables introduced in the context.
+  The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
+  $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
+    ]} with $m$ being the number of constructors of the type of
+  {\term}. Each variable introduced by {\tt destruct} in the context
+  of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
+  $p_{in_i}$ in order. If there are not enough names, {\tt destruct}
+  invents names for the remaining variables to introduce. More
+  generally, the $p_{ij}$ can be any disjunctive/conjunctive
+  introduction pattern (see Section~\ref{intros-pattern}). This
+  provides a concise notation for nested destruction.
+
+%  It is recommended to use this variant of {\tt destruct} for 
+%  robust proof scripts.
+
+\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn}
+
+  This behaves as {\tt destruct {\term}} but adds an equation between
+  {\term} and the value that {\term} takes in each of the possible
+  cases.  The name of the equation is chosen by Coq. If  
+  {\disjconjintropattern} is simply {\tt []}, it is automatically considered
+  as a disjunctive pattern of the appropriate size.
+
+\item{\tt destruct {\term} as {\disjconjintropattern} \_eqn: {\namingintropattern}}
+
+  This behaves as {\tt destruct {\term} as
+    {\disjconjintropattern} \_eqn} but use {\namingintropattern} to
+  name the equation (see Section~\ref{intros-pattern}). Note that spaces 
+  can generally be removed around {\tt \_eqn}.
+
+\item{\tt destruct {\term} with \bindinglist}
+
+  This behaves like \texttt{destruct {\term}} providing explicit
+  instances for the dependent premises of the type of {\term} (see
+  syntax of bindings in Section~\ref{Binding-list}).
+
+\item{\tt edestruct {\term}\tacindex{edestruct}}
+
+  This tactic behaves like \texttt{destruct {\term}} excepts that it
+  does not fail if the instance of a dependent premises of the type of
+  {\term} is not inferable. Instead, the unresolved instances are left
+  as existential variables to be inferred later, in the same way as
+  {\tt eapply} does (see Section~\ref{eapply-example}).
+
+\item{\tt destruct {\term$_1$} using {\term$_2$}}\\
+     {\tt destruct {\term$_1$} using {\term$_2$} with {\bindinglist}}
+
+  These are synonyms of {\tt induction {\term$_1$} using {\term$_2$}} and
+  {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}}.
+
+\item \texttt{destruct {\term} in {\occgoalset}}
+
+  This syntax is used for selecting which occurrences of {\term} the
+  case analysis has to be done on. The {\tt in {\occgoalset}} 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 case of the analysis is added to the
+  context of the subgoals corresponding to the cases (even
+  if no clause {\tt as {\namingintropattern}} is given).
+
+\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn: {\namingintropattern}  using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\
+     {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} \_eqn: {\namingintropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}
+
+  These are the general forms of {\tt destruct} and {\tt edestruct}.
+  They combine the effects of the {\tt with}, {\tt as}, {\tt using},
+  and {\tt in} clauses.
+
+\item{\tt case \term}\label{case}\tacindex{case}
+  
+  The tactic {\tt case} is a more basic tactic to perform case
+  analysis without recursion. It behaves as {\tt elim \term} but using
+  a case-analysis elimination principle and not a recursive one.
+
+\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. The effect of this tactic is similar to the effect of {\tt
+ destruct {\term} in |- *} with the exception that no new hypotheses 
+ are introduced in the context.
+
+\item {\tt case {\term} with {\bindinglist}}
+
+  Analogous to {\tt elim {\term} with {\bindinglist}} above.
+
+\item{\tt ecase {\term}\tacindex{ecase}}\\
+  {\tt ecase {\term} with {\bindinglist}}
+  
+  In case the type of {\term} has dependent premises, or dependent
+  premises whose values are not inferable from the {\tt with
+  {\bindinglist}} clause, {\tt ecase} turns them into existential
+  variables to be resolved later on.
+
+\item {\tt simple destruct \ident}\tacindex{simple destruct}
+  
+  This tactic behaves as {\tt intros until
+    {\ident}; case {\tt {\ident}}} when {\ident} is a quantified
+  variable of the goal.
+
+\item {\tt simple destruct {\num}}
+  
+  This tactic behaves as {\tt intros until
+    {\num}; case {\tt {\ident}}} where {\ident} is the name given by
+  {\tt intros until {\num}} to the {\num}-th non-dependent premise of
+  the goal.
+
+
+\end{Variants}
+
+\subsection{\tt intros {\intropattern} {\ldots} {\intropattern}
+\label{intros-pattern}
+\tacindex{intros \intropattern}}
+\index{Introduction patterns}
+\index{Naming introduction patterns}
+\index{Disjunctive/conjunctive introduction patterns}
+
+This extension of the tactic {\tt intros} combines introduction of
+variables or hypotheses and case analysis. An {\em introduction pattern} is
+either:
+\begin{itemize}
+\item A {\em naming introduction pattern}, i.e. either one of:
+  \begin{itemize}
+  \item the pattern \texttt{?}
+  \item the pattern \texttt{?\ident}
+  \item an identifier
+  \end{itemize}
+\item A {\em disjunctive/conjunctive introduction pattern}, i.e. either one of:
+  \begin{itemize}
+  \item a disjunction of lists of patterns:
+  {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
+  \item a conjunction of patterns: {\tt (} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt )}
+  \item a list of patterns {\tt (} $p_1$\ {\tt \&}\ {\ldots}\ {\tt \&}\ $p_n$ {\tt )}
+   for sequence of right-associative binary constructs
+  \end{itemize}
+\item the wildcard: {\tt \_}
+\item the rewriting orientations: {\tt ->} or {\tt <-}
+\end{itemize}
+
+Assuming a goal of type {\tt $Q$ -> $P$} (non dependent product), or
+of type {\tt forall $x$:$T$, $P$} (dependent product), the behavior of
+{\tt intros $p$} is defined inductively over the structure of the
+introduction pattern $p$:
+\begin{itemize}
+\item introduction on \texttt{?} performs the introduction, and lets {\Coq}
+  choose a fresh name for the variable;
+\item introduction on \texttt{?\ident} performs the introduction, and
+  lets {\Coq} choose a fresh name for the variable based on {\ident};
+\item introduction on \texttt{\ident} behaves as described in
+  Section~\ref{intro};
+\item introduction over a disjunction of list of patterns {\tt
+  [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots}
+    $p_{nm_n}$]} expects the product to be over an inductive type
+  whose number of constructors is $n$ (or more generally over a type
+  of conclusion an inductive type built from $n$ constructors,
+  e.g. {\tt C -> A$\backslash$/B if $n=2$}): it destructs the introduced
+  hypothesis as {\tt destruct} (see Section~\ref{destruct}) would and
+  applies on each generated subgoal the corresponding tactic;
+  \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive
+  pattern is part of a sequence of patterns and is not the last
+  pattern of the sequence, then {\Coq} completes the pattern so as all
+  the argument of the constructors of the inductive type are
+  introduced (for instance, the list of patterns {\tt [$\;$|$\;$] H}
+  applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same as
+  the list of patterns {\tt [$\,$|$\,$?$\,$] H});
+\item introduction over a conjunction of patterns {\tt ($p_1$, \ldots,
+  $p_n$)} expects the goal to be a product over an inductive type $I$ with a
+  single constructor that itself has at least $n$ arguments: it
+  performs a case analysis over the hypothesis, as {\tt destruct}
+  would, and applies the patterns $p_1$~\ldots~$p_n$ to the arguments
+  of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots},
+  $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots}
+  $p_n$]});
+\item introduction via {\tt ( $p_1$ \& \ldots \& $p_n$ )}
+  is a shortcut for introduction via
+  {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
+  hypothesis to be a sequence of right-associative binary inductive 
+  constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
+  hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
+  introduced via pattern {\tt (a \& x \& b \& c \& d)};
+\item introduction on the wildcard depends on whether the product is
+  dependent or not: in the non dependent case, it erases the
+  corresponding hypothesis (i.e. it behaves as an {\tt intro} followed
+  by a {\tt clear}, cf Section~\ref{clear}) while in the dependent
+  case, it succeeds and erases the variable only if the wildcard is
+  part of a more complex list of introduction patterns that also
+  erases the hypotheses depending on this variable;
+\item introduction over {\tt ->} (respectively {\tt <-}) expects the
+  hypothesis to be an equality and the right-hand-side (respectively
+  the left-hand-side) is replaced by the left-hand-side (respectively
+  the right-hand-side) in both the conclusion and the context of the goal;
+  if moreover the term to substitute is a variable, the hypothesis is
+  removed.
+\end{itemize}
+
+\Rem {\tt intros $p_1~\ldots~p_n$} is not equivalent to \texttt{intros
+  $p_1$;\ldots; intros $p_n$} for the following reasons:
+\begin{itemize}
+\item A wildcard pattern never succeeds when applied isolated on a
+  dependent product, while it succeeds as part of a list of
+  introduction patterns if the hypotheses that depends on it are
+  erased too.
+\item A disjunctive or conjunctive pattern followed by an introduction
+  pattern forces the introduction in the context of all arguments of
+  the constructors before applying the next pattern while a terminal
+  disjunctive or conjunctive pattern does not. Here is an example
+
+\begin{coq_example}
+Goal forall n:nat, n = 0 -> n = 0.
+intros [ | ] H.
+Show 2.
+Undo.
+intros [ | ]; intros H.
+Show 2.
+\end{coq_example}
+
+\end{itemize}
+
+\begin{coq_example}
+Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
+intros A B C [a| [_ c]] f.
+apply (f a).
+exact c.
+Qed.
+\end{coq_example}
+
+%\subsection[\tt FixPoint \dots]{\tt FixPoint \dots\tacindex{Fixpoint}}
+%Not yet documented.
+
+\subsection{\tt double induction \ident$_1$ \ident$_2$}
+%\tacindex{double induction}}
+This tactic is deprecated and should be replaced by {\tt induction \ident$_1$; induction \ident$_2$} (or {\tt induction \ident$_1$; destruct \ident$_2$} depending on the exact needs).
+
+%% This tactic applies to any goal. If the variables {\ident$_1$} and
+%% {\ident$_2$} of the goal have an inductive type, then this tactic
+%% performs double induction on these variables.  For instance, if the
+%% current goal is \verb+forall n m:nat, P n m+ then, {\tt double induction n
+%%   m} yields the four cases with their respective inductive hypotheses.
+
+%% In particular, for proving \verb+(P (S n) (S m))+, the generated induction
+%% hypotheses are \verb+(P (S n) m)+ and \verb+(m:nat)(P n m)+ (of the latter, 
+%% \verb+(P n m)+ and \verb+(P n (S m))+ are derivable).
+
+%% \Rem When the induction hypothesis \verb+(P (S n) m)+ is not
+%% needed, {\tt induction \ident$_1$; destruct \ident$_2$} produces
+%% more concise subgoals.
+
+\begin{Variant}
+
+\item {\tt double induction \num$_1$ \num$_2$}
+
+This tactic is deprecated and should be replaced by {\tt induction
+  \num$_1$; induction \num$_3$} where \num$_3$ is the result of
+\num$_2$-\num$_1$.
+
+%% This tactic applies to any goal. If the variables {\ident$_1$} and
+
+%% This applies double induction on the \num$_1^{th}$ and \num$_2^{th}$ {\it
+%% non dependent} premises of the goal. More generally, any combination of an
+%% {\ident} and a {\num} is valid.
+
+\end{Variant}
+
+\subsection{\tt dependent induction \ident
+  \tacindex{dependent induction}
+  \label{DepInduction}}
+
+The \emph{experimental} tactic \texttt{dependent induction} performs
+induction-inversion on an instantiated inductive predicate.
+One needs to first require the {\tt Coq.Program.Equality} module to use
+this tactic. The tactic is based on the BasicElim tactic by Conor
+McBride \cite{DBLP:conf/types/McBride00} and the work of Cristina Cornes
+around inversion \cite{DBLP:conf/types/CornesT95}. From an instantiated
+inductive predicate and a goal it generates an equivalent goal where the
+hypothesis has been generalized over its indexes which are then
+constrained by equalities to be the right instances. This permits to
+state lemmas without resorting to manually adding these equalities and
+still get enough information in the proofs. 
+A simple example is the following:
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example}
+Lemma le_minus : forall n:nat, n < 1 -> n = 0.
+intros n H ; induction H.
+\end{coq_example}
+
+Here we didn't get any information on the indexes to help fulfill this
+proof. The problem is that when we use the \texttt{induction} tactic
+we lose information on the hypothesis instance, notably that the second
+argument is \texttt{1} here. Dependent induction solves this problem by
+adding the corresponding equality to the context.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example}
+Require Import Coq.Program.Equality.
+Lemma le_minus : forall n:nat, n < 1 -> n = 0.
+intros n H ; dependent induction H.
+\end{coq_example}
+
+The subgoal is cleaned up as the tactic tries to automatically
+simplify the subgoals with respect to the generated equalities.
+In this enriched context it becomes possible to solve this subgoal.
+\begin{coq_example}
+reflexivity.
+\end{coq_example}
+
+Now we are in a contradictory context and the proof can be solved.
+\begin{coq_example}
+inversion H.
+\end{coq_example}
+
+This technique works with any inductive predicate.
+In fact, the \texttt{dependent induction} tactic is just a wrapper around
+the \texttt{induction} tactic. One can make its own variant by just
+writing a new tactic based on the definition found in
+\texttt{Coq.Program.Equality}. Common useful variants are the following,
+defined in the same file:
+
+\begin{Variants}
+\item {\tt dependent induction {\ident} generalizing {\ident$_1$} \dots
+    {\ident$_n$}}\tacindex{dependent induction \dots\ generalizing}
+  
+  Does dependent induction on the hypothesis {\ident} but first
+  generalizes the goal by the given variables so that they are
+  universally quantified in the goal. This is generally what one wants
+  to do with the variables that are inside some constructors in the
+  induction hypothesis. The other ones need not be further generalized.
+
+\item {\tt dependent destruction {\ident}}\tacindex{dependent destruction}
+  
+  Does the generalization of the instance {\ident} but uses {\tt destruct}
+  instead of {\tt induction} on the generalized hypothesis. This gives
+  results equivalent to {\tt inversion} or {\tt dependent inversion} if
+  the hypothesis is dependent.
+\end{Variants}
+
+A larger example of dependent induction and an explanation of the
+underlying technique are developed in section~\ref{dependent-induction-example}.
+
+\subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term
+\label{decompose}
+\tacindex{decompose}}
+
+This tactic allows to recursively decompose a
+complex proposition in order to obtain atomic ones.
+Example: 
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example}
+Lemma ex1 : forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
+intros A B C H; decompose [and or] H; assumption.
+\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
+
+{\tt decompose} does not work on right-hand sides of implications or products.
+
+\begin{Variants}
+  
+\item {\tt decompose sum \term}\tacindex{decompose sum}
+  This decomposes sum types (like \texttt{or}).
+\item {\tt decompose record \term}\tacindex{decompose record}
+  This decomposes record types (inductive types with one constructor,
+  like \texttt{and} and \texttt{exists} and those defined with the
+  \texttt{Record} macro, see Section~\ref{Record}).
+\end{Variants}
+
+
+\subsection{\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$).
+\tacindex{functional induction}
+\label{FunInduction}}
+
+The \emph{experimental} tactic \texttt{functional induction} performs
+case analysis and induction following the definition of a function. It
+makes use of a principle generated by \texttt{Function}
+(see Section~\ref{Function}) or \texttt{Functional Scheme}
+(see Section~\ref{FunScheme}).
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example}
+Functional Scheme minus_ind := Induction for minus Sort Prop.
+
+Lemma le_minus : forall n m:nat, (n - m <= n).
+intros n m.
+functional induction (minus n m); simpl; auto.
+\end{coq_example}
+\begin{coq_example*}
+Qed.
+\end{coq_example*}
+
+\Rem \texttt{(\qualid\ \term$_1$ \dots\ \term$_n$)} must be a correct
+full application of \qualid. In particular, the rules for implicit
+arguments are the same as usual. For example use \texttt{@\qualid} if
+you want to write implicit arguments explicitly.
+
+\Rem Parenthesis over \qualid \dots \term$_n$ are mandatory.
+
+\Rem \texttt{functional induction (f x1 x2 x3)} is actually a wrapper
+for \texttt{induction x1 x2 x3 (f x1 x2 x3) using \qualid} followed by
+a cleaning phase, where $\qualid$ is the induction principle
+registered for $f$ (by the \texttt{Function} (see Section~\ref{Function})
+or \texttt{Functional Scheme} (see Section~\ref{FunScheme}) command)
+corresponding to the sort of the goal.  Therefore \texttt{functional
+  induction} may fail if the induction scheme (\texttt{\qualid}) is
+not defined. See also Section~\ref{Function} for the function terms
+accepted by \texttt{Function}.
+
+\Rem There is a difference between obtaining an induction scheme for a
+function by using \texttt{Function} (see Section~\ref{Function}) and by
+using \texttt{Functional Scheme} after a normal definition using
+\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
+details.
+
+\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples},
+  \ref{sec:functional-inversion}}
+
+\begin{ErrMsgs}
+\item \errindex{Cannot find induction information on \qualid}
+
+  ~
+
+\item \errindex{Not the right number of induction arguments}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)
+   using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}}
+
+ Similar to \texttt{Induction} and \texttt{elim}
+ (see Section~\ref{Tac-induction}), allows to give explicitly the
+ induction principle and the values of dependent premises of the
+ elimination scheme, including \emph{predicates} for mutual induction
+ when {\qualid} is part of a mutually recursive definition.
+
+\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)
+    using \term$_{m+1}$ with {\vref$_1$} := {\term$_{n+1}$} \dots\
+    {\vref$_m$} := {\term$_n$}}
+
+  Similar to \texttt{induction} and \texttt{elim}
+  (see Section~\ref{Tac-induction}).
+
+\item All previous variants can be extended by the usual \texttt{as
+    \intropattern} construction, similar for example to
+  \texttt{induction} and \texttt{elim} (see Section~\ref{Tac-induction}).
+    
+\end{Variants}
+
+
+
+\section{Equality}
+
+These tactics use the equality {\tt eq:forall A:Type, A->A->Prop}
+defined in file {\tt Logic.v} (see Section~\ref{Equality}). The
+notation for {\tt eq}~$T~t~u$ is simply {\tt $t$=$u$} dropping the
+implicit type of $t$ and $u$.
+
+\subsection{\tt rewrite \term
+\label{rewrite}
+\tacindex{rewrite}}
+
+This tactic applies to any goal. The type of {\term}
+must have the form
+
+\texttt{forall (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} finds the first subterm matching
+\term$_1$ in the goal, resulting in instances \term$_1'$ and \term$_2'$
+and then replaces every occurrence of \term$_1'$ by \term$_2'$.
+Hence, some of the variables x$_i$ are
+solved by unification, and some of the types \texttt{A}$_1$, \dots,
+\texttt{A}$_n$ become new subgoals.
+
+% \Rem In case the type of  
+% \term$_1$ contains occurrences of variables bound in the
+% type of \term, the tactic tries first to find a subterm of the goal
+% which matches this term in order to find a closed instance \term$'_1$
+% of \term$_1$, and then all instances of \term$'_1$ will be replaced.
+
+\begin{ErrMsgs}
+\item \errindex{The term provided does not end with an equation}
+
+\item \errindex{Tactic generated a subgoal identical to the original goal}\\
+This happens if \term$_1$ does not occur in the goal.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt rewrite -> {\term}}\tacindex{rewrite ->}\\
+  Is equivalent to {\tt rewrite \term}
+
+\item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\
+  Uses the equality \term$_1${\tt=}\term$_2$ from right to left
+
+\item {\tt rewrite {\term} in \textit{clause}}
+  \tacindex{rewrite \dots\ in}\\
+  Analogous to {\tt rewrite {\term}} but rewriting is done following
+  \textit{clause} (similarly to \ref{Conversion-tactics}). For
+  instance:
+  \begin{itemize}
+  \item \texttt{rewrite H in H1} will rewrite \texttt{H} in the hypothesis
+    \texttt{H1} instead of the current goal.
+  \item \texttt{rewrite H in H1 at 1, H2 at - 2 |- *} means \texttt{rewrite H; rewrite H in H1 at 1;
+      rewrite H in H2 at - 2}. In particular a failure will happen if any of
+    these three simpler tactics fails. 
+  \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
+      H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
+    as soon as at least one of these simpler tactics succeeds.
+  \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H} 
+    and \texttt{rewrite H in * |-} that succeeds if at
+    least one of these two tactics succeeds. 
+  \end{itemize}
+  Orientation {\tt ->} or {\tt <-} can be
+  inserted before the term to rewrite.
+
+\item {\tt rewrite {\term} at {\occlist}}
+  \tacindex{rewrite \dots\ at}
+
+  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's equality, so one has to 
+  \texttt{Import Setoid} to use this variant.
+
+\item {\tt rewrite {\term} by {\tac}}
+  \tacindex{rewrite \dots\ by}
+
+  Use {\tac} to completely solve the side-conditions arising from the
+  rewrite.
+
+\item {\tt rewrite $\term_1$, \ldots, $\term_n$}\\
+  Is equivalent to the $n$ successive tactics {\tt rewrite $\term_1$}
+  up to {\tt rewrite $\term_n$}, each one working on the first subgoal
+  generated by the previous one.
+  Orientation {\tt ->} or {\tt <-} can be
+  inserted before each term to rewrite. One unique \textit{clause}
+  can be added at the end after the keyword {\tt in}; it will 
+  then affect all rewrite operations.
+
+\item In all forms of {\tt rewrite} described above, a term to rewrite
+  can be immediately prefixed by one of the following modifiers:
+  \begin{itemize}
+  \item {\tt ?} : the tactic {\tt rewrite ?$\term$} performs the
+    rewrite of $\term$  as many times as possible (perhaps zero time).
+    This form never fails. 
+  \item {\tt $n$?} : works similarly, except that it will do at most 
+   $n$ rewrites. 
+  \item {\tt !} : works as {\tt ?}, except that at least one rewrite 
+    should succeed, otherwise the tactic fails. 
+  \item {\tt $n$!} (or simply {\tt $n$}) : precisely $n$ rewrites 
+    of $\term$ will be done, leading to failure if these $n$ rewrites are not possible. 
+  \end{itemize}
+
+\item {\tt erewrite {\term}\tacindex{erewrite}}
+
+This tactic works as {\tt rewrite {\term}} but turning unresolved
+bindings into existential variables, if any, instead of failing. It has
+the same variants as {\tt rewrite} has.
+
+\end{Variants}
+
+
+\subsection{\tt cutrewrite -> \term$_1$ = \term$_2$
+\label{cutrewrite}
+\tacindex{cutrewrite}}
+
+This tactic acts like {\tt replace {\term$_1$} with {\term$_2$}}
+(see below).
+
+\subsection{\tt replace {\term$_1$} with {\term$_2$}
+\label{tactic:replace}
+\tacindex{replace \dots\ with}}
+
+This tactic applies to any goal. It replaces all free occurrences of
+{\term$_1$} in the current goal with {\term$_2$} and generates the
+equality {\term$_2$}{\tt =}{\term$_1$} as a subgoal. This equality is
+automatically solved if it occurs amongst the assumption, or if its
+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$} by \tac}\\ This acts
+  as {\tt replace {\term$_1$} with {\term$_2$}} but applies {\tt \tac}
+  to solve the generated subgoal {\tt \term$_2$=\term$_1$}.
+\item {\tt replace {\term}}\\ Replace {\term} with {\term'} using the
+  first assumption whose type has the form {\tt \term=\term'} or {\tt
+    \term'=\term}
+\item {\tt replace -> {\term}}\\ Replace {\term} with {\term'} using the
+  first assumption whose type has the form {\tt \term=\term'}
+\item {\tt replace <- {\term}}\\ Replace {\term} with {\term'} using the
+  first assumption whose type has the form {\tt \term'=\term}
+\item {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} }\\
+    {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} by \tac }\\ 
+    {\tt replace {\term} \textit{clause}}\\ 
+    {\tt replace -> {\term} \textit{clause}}\\ 
+    {\tt replace <- {\term} \textit{clause}}\\ 
+    Act as before but the replacements take place in
+    \textit{clause}~(see Section~\ref{Conversion-tactics}) and not only
+    in the conclusion of the goal.\\
+    The  \textit{clause} argument must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
+\end{Variants}
+
+\subsection{\tt reflexivity
+\label{reflexivity}
+\tacindex{reflexivity}}
+
+This tactic applies to a goal which has the form {\tt t=u}. It checks
+that {\tt t} and {\tt u} are convertible and then solves the goal.
+It is equivalent to {\tt apply refl\_equal}.
+
+\begin{ErrMsgs}
+\item \errindex{The conclusion is not a substitutive equation}
+\item \errindex{Impossible to unify \dots\ with \dots.}
+\end{ErrMsgs}
+
+\subsection{\tt symmetry
+\tacindex{symmetry}
+\tacindex{symmetry in}}
+This tactic applies to a goal which has the form {\tt t=u} and changes it
+into {\tt u=t}.
+
+\variant {\tt symmetry in {\ident}}\\
+If the statement of the hypothesis {\ident} has the form {\tt t=u},
+the tactic changes it to {\tt u=t}.
+
+\subsection{\tt transitivity \term
+\tacindex{transitivity}}
+This tactic applies to a goal which has the form {\tt t=u}
+and transforms it into the two subgoals 
+{\tt t={\term}} and {\tt {\term}=u}.
+
+\subsection{\tt subst {\ident}
+\tacindex{subst}}
+
+This tactic applies to a goal which has \ident\ in its context and
+(at least) one hypothesis, say {\tt H}, of type {\tt
+  \ident=t} or {\tt t=\ident}. Then it replaces 
+\ident\ by {\tt t} everywhere in the goal (in the hypotheses 
+and in the conclusion) and clears \ident\ and {\tt H} from the context.
+
+\Rem 
+When several hypotheses have the form {\tt \ident=t} or {\tt
+  t=\ident}, the first one is used. 
+
+\begin{Variants}
+  \item {\tt subst \ident$_1$ \dots \ident$_n$} \\
+    Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}.
+  \item {\tt subst} \\
+    Applies {\tt subst} repeatedly to all identifiers from the context
+    for which an equality exists.
+\end{Variants}
+
+\subsection[{\tt stepl {\term}}]{{\tt stepl {\term}}\tacindex{stepl}}
+
+This tactic is for chaining rewriting steps. It assumes a goal of the
+form ``$R$ {\term}$_1$ {\term}$_2$'' where $R$ is a binary relation
+and relies on a database of lemmas of the form {\tt forall} $x$ $y$
+$z$, $R$ $x$ $y$ {\tt ->} $eq$ $x$ $z$ {\tt ->} $R$ $z$ $y$ where $eq$
+is typically a setoid equality. The application of {\tt stepl {\term}}
+then replaces the goal by ``$R$ {\term} {\term}$_2$'' and adds a new
+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 {\term}.}
+\end{quote}
+
+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}).
+
+\tacindex{stepr}
+\comindex{Declare Right Step}
+\begin{Variants}
+\item{\tt stepl {\term} by {\tac}}\\
+This applies {\tt stepl {\term}} then applies {\tac} to the second goal.
+
+\item{\tt stepr {\term}}\\
+     {\tt stepr {\term} by {\tac}}\\
+This behaves as {\tt stepl} but on the right-hand-side of the binary relation.
+Lemmas are expected to be of the form
+``{\tt forall} $x$ $y$
+$z$, $R$ $x$ $y$ {\tt ->} $eq$ $y$ $z$ {\tt ->} $R$ $x$ $z$''
+and are registered using the command
+\begin{quote}
+{\tt Declare Right Step {\term}.}
+\end{quote}
+\end{Variants}
+
+
+\subsection{\tt f\_equal
+\label{f-equal}
+\tacindex{f\_equal}}
+
+This tactic applies to a goal of the form $f\ a_1\ \ldots\ a_n = f'\
+a'_1\ \ldots\ a'_n$. Using {\tt f\_equal} on such a goal leads to
+subgoals $f=f'$ and $a_1=a'_1$ and so on up to $a_n=a'_n$. Amongst 
+these subgoals, the simple ones (e.g. provable by
+reflexivity or congruence) are automatically solved by {\tt f\_equal}.
+
+
+\section{Equality and inductive sets}
+
+We describe in this section some special purpose tactics dealing with
+equality and inductive sets or types. These tactics use the equality
+{\tt eq:forall (A:Type), A->A->Prop}, simply written with the
+infix symbol {\tt =}.
+
+\subsection{\tt decide equality
+\label{decideequality}
+\tacindex{decide equality}}
+
+This tactic solves a goal of the form
+{\tt forall $x$ $y$:$R$, \{$x$=$y$\}+\{\verb|~|$x$=$y$\}}, where $R$
+is an inductive type such that its constructors do not take proofs or
+functions as arguments, nor objects in dependent types.
+
+\begin{Variants}
+\item {\tt decide equality {\term}$_1$ {\term}$_2$ }.\\
+ Solves a goal of the form {\tt \{}\term$_1${\tt =}\term$_2${\tt
+\}+\{\verb|~|}\term$_1${\tt =}\term$_2${\tt \}}.
+\end{Variants}
+
+\subsection{\tt compare \term$_1$ \term$_2$
+\tacindex{compare}}
+
+This tactic compares two given objects \term$_1$ and \term$_2$ 
+of an inductive datatype. If $G$ is the current goal, it leaves the sub-goals
+\term$_1${\tt =}\term$_2$ {\tt ->} $G$ and \verb|~|\term$_1${\tt =}\term$_2$
+{\tt ->} $G$. The type
+of \term$_1$ and \term$_2$ must satisfy the same restrictions as in the tactic
+\texttt{decide equality}.
+
+\subsection{\tt discriminate {\term}
+\label{discriminate}
+\tacindex{discriminate}
+\tacindex{ediscriminate}}
+
+This tactic proves any goal from an assumption stating that two
+structurally different terms of an inductive set are equal. For
+example, from {\tt (S (S O))=(S O)} we can derive by absurdity any
+proposition.
+
+The argument {\term} is assumed to be a proof of a statement
+of conclusion {\tt{\term$_1$} = {\term$_2$}} with {\term$_1$} and
+{\term$_2$} being elements of an inductive set.  To build the proof,
+the tactic traverses the normal forms\footnote{Reminder: opaque
+  constants will not be expanded by $\delta$ reductions} of
+{\term$_1$} and {\term$_2$} looking for a couple of subterms {\tt u}
+and {\tt w} ({\tt u} subterm of the normal form of {\term$_1$} and
+{\tt w} subterm of the normal form of {\term$_2$}), placed at the same
+positions and whose head symbols are two different constructors. If
+such a couple of subterms exists, then the proof of the current goal
+is completed, otherwise the tactic fails.
+
+\Rem The syntax {\tt discriminate {\ident}} can be used to refer to a
+hypothesis quantified in the goal. In this case, the quantified
+hypothesis whose name is {\ident} is first introduced in the local
+context using \texttt{intros until \ident}.
+
+\begin{ErrMsgs}
+\item \errindex{No primitive equality found}
+\item \errindex{Not a discriminable equality}
+\end{ErrMsgs}  
+
+\begin{Variants}
+\item \texttt{discriminate} \num
+
+  This does the same thing as \texttt{intros until \num} followed by
+  \texttt{discriminate \ident} where {\ident} is the identifier for
+  the last introduced hypothesis.
+
+\item \texttt{discriminate} {\term} {\tt with} {\bindinglist}
+
+  This does the same thing as \texttt{discriminate {\term}} but using
+the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{ediscriminate} \num\\
+      \texttt{ediscriminate} {\term} \zeroone{{\tt with} {\bindinglist}}
+
+  This works the same as {\tt discriminate} but if the type of {\term},
+  or the type of the hypothesis referred to by {\num}, has uninstantiated
+  parameters, these parameters are left as existential variables.
+
+\item \texttt{discriminate}
+
+  This behaves like {\tt discriminate {\ident}} if {\ident} is the
+  name of an hypothesis to which {\tt discriminate} is applicable; if
+  the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$},
+  this behaves as {\tt intro {\ident}; injection {\ident}}.
+
+  \begin{ErrMsgs}
+  \item \errindex{No discriminable equalities} \\
+  occurs when the goal does not verify the expected preconditions.
+  \end{ErrMsgs}
+\end{Variants}
+
+\subsection{\tt injection {\term}
+\label{injection}
+\tacindex{injection}
+\tacindex{einjection}}
+
+The {\tt injection} tactic is based on the fact that constructors of
+inductive sets are injections. That means that if $c$ is a constructor
+of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two
+terms that are equal then $~\vec{t_1}$ and $~\vec{t_2}$ are equal
+too.
+
+If {\term} is a proof of a statement of conclusion
+ {\tt {\term$_1$} = {\term$_2$}},
+then {\tt injection} applies injectivity as deep as possible to
+derive the equality of all the subterms of {\term$_1$} and {\term$_2$}
+placed in the same positions. For example, from {\tt (S
+  (S n))=(S (S (S m))} we may derive {\tt n=(S m)}.  To use this
+tactic {\term$_1$} and {\term$_2$} should be elements of an inductive
+set and they should be neither explicitly equal, nor structurally
+different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are
+their respective normal forms, then:
+\begin{itemize}
+\item {\tt n$_1$} and {\tt n$_2$} should not be syntactically equal,
+\item there must not exist any pair of subterms {\tt u} and {\tt w},
+  {\tt u} subterm of {\tt n$_1$} and {\tt w} subterm of {\tt n$_2$} ,
+  placed in the same positions and having different constructors as
+  head symbols.
+\end{itemize}
+If these conditions are satisfied, then, the tactic derives the
+equality of all the subterms of {\term$_1$} and {\term$_2$} placed in
+the same positions and puts them as antecedents of the current goal.
+
+\Example Consider the following goal:
+
+\begin{coq_example*}
+Inductive list : Set :=
+  | nil : list
+  | cons : nat -> list -> list.
+Variable P : list -> Prop.
+\end{coq_example*}
+\begin{coq_eval}
+Lemma ex :
+ forall (l:list) (n:nat), P nil -> cons n l = cons 0 nil -> P l.
+intros l n H H0.
+\end{coq_eval}
+\begin{coq_example}
+Show.
+injection H0.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+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 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 
+(see \ref{Scheme}).
+
+\Rem If some quantified hypothesis of the goal is named {\ident}, then
+{\tt injection {\ident}} first introduces the hypothesis in the local
+context using \texttt{intros until \ident}.
+
+\begin{ErrMsgs}
+\item \errindex{Not a projectable equality but a discriminable one}
+\item \errindex{Nothing to do, it is an equality between convertible terms}
+\item \errindex{Not a primitive equality}
+\end{ErrMsgs}
+
+\begin{Variants}
+\item \texttt{injection} \num{}
+
+  This does the same thing as \texttt{intros until \num} followed by
+\texttt{injection \ident} where {\ident} is the identifier for the last
+introduced hypothesis.
+
+\item \texttt{injection} \term{} {\tt with} {\bindinglist}
+
+  This does the same as \texttt{injection {\term}} but using
+  the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{einjection} \num\\
+      \texttt{einjection} \term{} \zeroone{{\tt with} {\bindinglist}}
+
+  This works the same as {\tt injection} but if the type of {\term},
+  or the type of the hypothesis referred to by {\num}, has uninstantiated
+  parameters, these parameters are left as existential variables.
+
+\item{\tt injection}
+  
+  If the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$},
+  this behaves as {\tt intro {\ident}; injection {\ident}}.
+  
+  \ErrMsg \errindex{goal does not satisfy the expected preconditions}
+
+\item \texttt{injection} \term{} \zeroone{{\tt with} {\bindinglist}} \texttt{as} \nelist{\intropattern}{}\\
+\texttt{injection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{injection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{einjection} \term{} \zeroone{{\tt with} {\bindinglist}} \texttt{as} \nelist{\intropattern}{}\\
+\texttt{einjection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\texttt{einjection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
+\tacindex{injection \ldots{} as}
+ 
+These variants apply \texttt{intros} \nelist{\intropattern}{} after
+the call to \texttt{injection} or \texttt{einjection}.
+
+\end{Variants}
+
+\subsection{\tt simplify\_eq {\term}
+\tacindex{simplify\_eq}
+\tacindex{esimplify\_eq}
+\label{simplify-eq}}
+
+Let {\term} be the proof of a statement of conclusion {\tt
+  {\term$_1$}={\term$_2$}}. If {\term$_1$} and
+{\term$_2$} are structurally different (in the sense described for the
+tactic {\tt discriminate}), then the tactic {\tt simplify\_eq} behaves as {\tt
+  discriminate {\term}}, otherwise it behaves as {\tt injection
+  {\term}}.
+
+\Rem If some quantified hypothesis of the goal is named {\ident}, then
+{\tt simplify\_eq {\ident}} first introduces the hypothesis in the local
+context using \texttt{intros until \ident}.
+
+\begin{Variants}
+\item \texttt{simplify\_eq} \num
+
+  This does the same thing as \texttt{intros until \num} then
+\texttt{simplify\_eq \ident} where {\ident} is the identifier for the last
+introduced hypothesis.
+
+\item \texttt{simplify\_eq} \term{} {\tt with} {\bindinglist}
+
+  This does the same as \texttt{simplify\_eq {\term}} but using
+  the given bindings to instantiate parameters or hypotheses of {\term}.
+
+\item \texttt{esimplify\_eq} \num\\
+      \texttt{esimplify\_eq} \term{} \zeroone{{\tt with} {\bindinglist}}
+
+  This works the same as {\tt simplify\_eq} but if the type of {\term},
+  or the type of the hypothesis referred to by {\num}, has uninstantiated
+  parameters, these parameters are left as existential variables.
+
+\item{\tt simplify\_eq}
+
+If the current goal has form $t_1\verb=<>=t_2$, it behaves as
+\texttt{intro {\ident}; simplify\_eq {\ident}}.
+\end{Variants}
+
+\subsection{\tt dependent rewrite -> {\ident}
+\tacindex{dependent rewrite ->}
+\label{dependent-rewrite}}
+
+This tactic applies to any goal.  If \ident\ has type 
+\verb+(existT B a b)=(existT B a' b')+ 
+in the local context (i.e. each term of the
+equality has a sigma type $\{ a:A~ \&~(B~a)\}$) this tactic rewrites
+\verb+a+ into \verb+a'+ and \verb+b+ into \verb+b'+ in the current
+goal. This tactic works even if $B$ is also a sigma type.  This kind
+of equalities between dependent pairs may be derived by the injection
+and inversion tactics.
+
+\begin{Variants}
+\item{\tt dependent rewrite <- {\ident}}
+\tacindex{dependent rewrite <-} \\
+Analogous to {\tt dependent rewrite ->} but uses the equality from
+right to left.
+\end{Variants}
+
+\section{Inversion
+\label{inversion}}
+
+\subsection{\tt inversion {\ident}
+\tacindex{inversion}}
+
+Let the type of \ident~ in the local context be $(I~\vec{t})$,
+where $I$ is a (co)inductive predicate. Then,
+\texttt{inversion} applied to \ident~ derives for each possible
+constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary
+conditions that should hold for the instance $(I~\vec{t})$ to be
+proved by $c_i$.
+
+\Rem If {\ident} does not denote a hypothesis in the local context
+but refers to a hypothesis quantified in the goal, then the
+latter is first introduced in the local context using
+\texttt{intros until \ident}.
+
+\begin{Variants}
+\item \texttt{inversion} \num
+  
+  This does the same thing as \texttt{intros until \num} then
+  \texttt{inversion \ident} where {\ident} is the identifier for the
+  last introduced hypothesis.
+
+\item \tacindex{inversion\_clear} \texttt{inversion\_clear} \ident
+
+  This behaves as \texttt{inversion} and then erases \ident~ from the
+  context.
+
+\item \tacindex{inversion \dots\ as} \texttt{inversion} {\ident} \texttt{as} {\intropattern}
+  
+  This behaves as \texttt{inversion} but using names in
+  {\intropattern} for naming hypotheses. The {\intropattern} must have
+  the form {\tt [} $p_{11}$ \ldots $p_{1n_1}$ {\tt |} {\ldots} {\tt |}
+  $p_{m1}$ \ldots $p_{mn_m}$ {\tt ]} with $m$ being the number of
+  constructors of the type of {\ident}. Be careful that the list must
+  be of length $m$ even if {\tt inversion} discards some cases (which
+  is precisely one of its roles): for the discarded cases, just use an
+  empty list (i.e. $n_i=0$).
+
+  The arguments of the $i^{th}$ constructor and the
+  equalities that {\tt inversion} introduces in the context of the
+  goal corresponding to the $i^{th}$ constructor, if it exists, get
+  their names from the list $p_{i1}$ \ldots $p_{in_i}$ in order. If
+  there are not enough names, {\tt induction} invents names for the
+  remaining variables to introduce. In case an equation splits into
+  several equations (because {\tt inversion} applies {\tt injection}
+  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 subequalities
+  obtained from splitting the original equation. Here is an example.
+
+\begin{coq_eval}
+Require Import List.
+\end{coq_eval}
+
+\begin{coq_example}
+Inductive contains0 : list nat -> Prop :=
+  | in_hd : forall l, contains0 (0 :: l)
+  | in_tl : forall l b, contains0 l -> contains0 (b :: l).
+Goal forall l:list nat, contains0 (1 :: l) -> contains0 l.
+intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ].
+\end{coq_example}
+
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+\item \texttt{inversion} {\num} {\tt as} {\intropattern} 
+
+  This allows to name the hypotheses introduced by
+  \texttt{inversion} {\num} in the context.
+
+\item \tacindex{inversion\_cleardots\ as} \texttt{inversion\_clear}
+  {\ident} {\tt as} {\intropattern}  
+
+  This allows to name the hypotheses introduced by
+  \texttt{inversion\_clear} in the context.
+  
+\item \tacindex{inversion \dots\ in} \texttt{inversion } {\ident}
+  \texttt{in} \ident$_1$ \dots\ \ident$_n$
+
+  Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This
+  tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and
+  then performing \texttt{inversion}.
+  
+\item \tacindex{inversion \dots\ as \dots\ in} \texttt{inversion }
+  {\ident} {\tt as} {\intropattern} \texttt{in} \ident$_1$ \dots\ 
+  \ident$_n$
+  
+  This allows to name the hypotheses introduced in the context by
+  \texttt{inversion} {\ident} \texttt{in} \ident$_1$ \dots\ 
+  \ident$_n$.
+  
+\item \tacindex{inversion\_clear \dots\ in} \texttt{inversion\_clear}
+  {\ident} \texttt{in} \ident$_1$ \ldots \ident$_n$
+ 
+  Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This
+  tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and
+  then performing {\tt inversion\_clear}.
+  
+\item \tacindex{inversion\_clear \dots\ as \dots\ in}
+  \texttt{inversion\_clear} {\ident} \texttt{as} {\intropattern}
+  \texttt{in} \ident$_1$ \ldots \ident$_n$
+
+  This allows to name the hypotheses introduced in the context by
+  \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ \ldots
+  \ident$_n$.
+
+\item \tacindex{dependent inversion} \texttt{dependent inversion}
+  {\ident}  
+  
+  That must be used when \ident\ appears in the current goal.  It acts
+  like \texttt{inversion} and then substitutes \ident\ for the
+  corresponding term in the goal.
+  
+\item \tacindex{dependent inversion \dots\ as } \texttt{dependent
+    inversion} {\ident} \texttt{as} {\intropattern} 
+  
+  This allows to name the hypotheses introduced in the context by
+  \texttt{dependent inversion} {\ident}.
+
+\item \tacindex{dependent inversion\_clear} \texttt{dependent
+    inversion\_clear} {\ident} 
+  
+  Like \texttt{dependent inversion}, except that {\ident} is cleared
+  from the local context.
+
+\item \tacindex{dependent inversion\_clear \dots\ as}
+  \texttt{dependent inversion\_clear} {\ident}\texttt{as} {\intropattern}
+  
+  This allows to name the hypotheses introduced in the context by
+  \texttt{dependent inversion\_clear} {\ident}.
+
+\item \tacindex{dependent inversion \dots\ with} \texttt{dependent
+    inversion } {\ident} \texttt{ with } \term  
+  
+  This variant allows you to specify the generalization of the goal. It
+  is useful when the system fails to generalize the goal automatically. If
+  {\ident} has type $(I~\vec{t})$ and $I$ has type
+  $forall (\vec{x}:\vec{T}), s$,   then \term~  must be of type
+  $I:forall (\vec{x}:\vec{T}), I~\vec{x}\to s'$ where $s'$ is the
+  type of the goal.
+
+\item \tacindex{dependent inversion \dots\ as \dots\ with}
+  \texttt{dependent inversion } {\ident} \texttt{as} {\intropattern}
+  \texttt{ with } \term  
+  
+  This allows to name the hypotheses introduced in the context by
+  \texttt{dependent inversion } {\ident} \texttt{ with } \term.
+
+\item \tacindex{dependent inversion\_clear \dots\ with}
+  \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term 
+  
+  Like \texttt{dependent inversion \dots\ with} but clears {\ident} from
+  the local context.
+
+\item \tacindex{dependent inversion\_clear \dots\ as \dots\ with}
+  \texttt{dependent inversion\_clear } {\ident} \texttt{as}
+  {\intropattern} \texttt{ with } \term 
+  
+  This allows to name the hypotheses introduced in the context by
+  \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term.
+
+\item \tacindex{simple inversion} \texttt{simple inversion} {\ident}
+  
+  It is a very primitive inversion tactic that derives all the necessary
+  equalities  but it does not simplify the  constraints as
+  \texttt{inversion} does.
+
+\item \tacindex{simple inversion \dots\ as} \texttt{simple inversion}
+  {\ident} \texttt{as} {\intropattern} 
+  
+  This allows to name the hypotheses introduced in the context by
+  \texttt{simple inversion}.
+
+\item \tacindex{inversion \dots\ using} \texttt{inversion} \ident
+  \texttt{ using} \ident$'$  
+  
+  Let {\ident} have type $(I~\vec{t})$ ($I$ an inductive
+  predicate) in the local context, and \ident$'$ be a (dependent) inversion
+  lemma. Then, this tactic refines the current goal with the specified
+  lemma.
+
+\item \tacindex{inversion \dots\ using \dots\ in} \texttt{inversion}
+  {\ident} \texttt{using} \ident$'$ \texttt{in} \ident$_1$\dots\ \ident$_n$
+  
+  This tactic behaves as generalizing \ident$_1$\dots\ \ident$_n$,
+  then doing \texttt{inversion} {\ident} \texttt{using} \ident$'$.
+
+\end{Variants}
+
+\SeeAlso~\ref{inversion-examples} for detailed examples
+
+\subsection{\tt Derive Inversion {\ident} with
+  ${\tt forall (}\vec{x}{\tt :}\vec{T}{\tt),} I~\vec{t}$ Sort \sort
+\label{Derive-Inversion}
+\comindex{Derive Inversion}}
+
+This command generates an inversion principle for the
+\texttt{inversion \dots\ using} tactic.
+Let $I$ be an inductive predicate and $\vec{x}$ the variables
+occurring in $\vec{t}$. This command generates and stocks the
+inversion lemma for the sort \sort~ corresponding to the instance
+$forall (\vec{x}:\vec{T}), I~\vec{t}$ with the name {\ident} in the {\bf
+global} environment. When applied it is equivalent to have inverted
+the instance with the tactic {\tt inversion}.
+
+\begin{Variants}
+\item \texttt{Derive Inversion\_clear} {\ident} \texttt{with}
+  \comindex{Derive Inversion\_clear}
+  $forall (\vec{x}:\vec{T}), I~\vec{t}$ \texttt{Sort} \sort~ \\ 
+  \index{Derive Inversion\_clear \dots\ with}
+  When applied it is equivalent to having
+  inverted the instance with the tactic \texttt{inversion}
+  replaced by the tactic \texttt{inversion\_clear}.
+\item \texttt{Derive Dependent Inversion} {\ident} \texttt{with}
+  $forall (\vec{x}:\vec{T}), I~\vec{t}$ \texttt{Sort} \sort~\\
+  \comindex{Derive Dependent Inversion}
+  When applied it is equivalent to having
+  inverted the instance with the tactic \texttt{dependent inversion}.
+\item \texttt{Derive Dependent Inversion\_clear} {\ident} \texttt{with}
+  $forall (\vec{x}:\vec{T}), I~\vec{t}$ \texttt{Sort} \sort~\\
+  \comindex{Derive Dependent Inversion\_clear}
+  When applied it is equivalent to having
+  inverted the instance with the tactic \texttt{dependent inversion\_clear}.
+\end{Variants}
+
+\SeeAlso \ref{inversion-examples} for examples
+
+
+
+\subsection[\tt functional inversion \ident]{\tt functional inversion \ident\label{sec:functional-inversion}}
+
+\texttt{functional inversion} is a \emph{highly} experimental tactic
+which performs inversion on hypothesis \ident\ of the form
+\texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ =
+  \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been
+defined using \texttt{Function} (see Section~\ref{Function}).
+
+\begin{ErrMsgs}
+\item \errindex{Hypothesis {\ident} must contain at least one Function}
+\item \errindex{Cannot find inversion information for hypothesis \ident}
+  This error may be raised when  some inversion lemma failed to be
+  generated by Function.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt functional inversion \num}
+
+  This does the same thing as \texttt{intros until \num} then
+  \texttt{functional inversion \ident} where {\ident} is the
+  identifier for the last introduced hypothesis.
+\item {\tt functional inversion \ident\ \qualid}\\
+  {\tt functional inversion \num\ \qualid}
+
+  In case the hypothesis {\ident} (or {\num}) has a type of the form
+  \texttt{\qualid$_1$\ \term$_1$\dots\term$_n$\ =\ \qualid$_2$\
+    \term$_{n+1}$\dots\term$_{n+m}$} where \qualid$_1$ and \qualid$_2$
+  are valid candidates to functional inversion, this variant allows to
+  choose which must be inverted.
+\end{Variants}
+
+
+
+\subsection{\tt quote \ident
+\tacindex{quote}
+\index{2-level approach}}
+
+This kind of inversion has nothing to do with the tactic
+\texttt{inversion} above. This tactic does \texttt{change (\ident\
+  t)}, where \texttt{t} is a term built in order to ensure the
+convertibility. In other words, it does inversion of the function
+\ident. This function must be a fixpoint on a simple recursive
+datatype: see~\ref{quote-examples} for the full details.
+
+\begin{ErrMsgs}
+\item \errindex{quote: not a simple fixpoint}\\
+  Happens when \texttt{quote} is not able to perform inversion properly.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item \texttt{quote {\ident} [ \ident$_1$ \dots \ident$_n$ ]}\\
+  All terms that are built only with \ident$_1$ \dots \ident$_n$ will be
+  considered by \texttt{quote} as constants rather than variables.
+\end{Variants}
+
+% En attente d'un moyen de valoriser les fichiers de demos
+% \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} in the distribution
+
+\section[Classical tactics]{Classical tactics\label{ClassicalTactics}}
+
+In order to ease the proving process, when the {\tt Classical} module is loaded. A few more tactics are available. Make sure to load the module using the \texttt{Require Import} command.
+
+\subsection{{\tt classical\_left, classical\_right} \tacindex{classical\_left} \tacindex{classical\_right}}
+
+The tactics \texttt{classical\_left} and \texttt{classical\_right} are the analog of the \texttt{left} and \texttt{right} but using classical logic. They can only be used for disjunctions.
+Use  \texttt{classical\_left} to prove the left part of the disjunction with the assumption that the negation of right part holds. 
+Use \texttt{classical\_right} to prove the right part of the disjunction with the assumption that the negation of left part holds. 
+
+\section{Automatizing
+\label{Automatizing}}
+
+\subsection{\tt auto
+\label{auto}
+\tacindex{auto}}
+
+This tactic implements a Prolog-like resolution procedure to solve the
+current goal. It first tries to solve the goal using the {\tt
+  assumption} tactic, then it reduces the goal to an atomic one using
+{\tt intros} and introducing the newly generated hypotheses as hints.
+Then it looks at the list of tactics associated to the head symbol of
+the goal and tries to apply one of them (starting from the tactics
+with lower cost). This process is recursively applied to the generated
+subgoals. 
+
+By default, \texttt{auto} only uses the hypotheses of the current goal and the
+hints of the database named {\tt core}. 
+
+\begin{Variants}
+
+\item  {\tt auto \num}
+
+  Forces the search depth to be \num. The maximal search depth is 5 by
+  default. 
+
+\item {\tt auto with \ident$_1$ \dots\ \ident$_n$}
+  
+  Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to
+  the database {\tt core}. See Section~\ref{Hints-databases} for the
+  list of pre-defined databases and the way to create or extend a
+  database.  This option can be combined with the previous one.
+
+\item {\tt auto with *}
+
+  Uses all existing hint databases, minus the special database
+  {\tt v62}. See Section~\ref{Hints-databases}
+
+\item \texttt{auto using \nterm{lemma}$_1$ , \ldots , \nterm{lemma}$_n$}
+
+  Uses \nterm{lemma}$_1$, \ldots, \nterm{lemma}$_n$ in addition to
+  hints (can be combined with the \texttt{with \ident} option). If
+  $lemma_i$ is an inductive type, it is the collection of its
+  constructors which is added as hints.
+
+\item \texttt{auto using \nterm{lemma}$_1$ , \ldots , \nterm{lemma}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+
+  This combines the effects of the {\tt using} and {\tt with} options.
+
+\item {\tt trivial}\tacindex{trivial}
+
+  This tactic is a restriction of {\tt auto} that is not recursive and 
+  tries only hints which cost 0. Typically it solves trivial
+  equalities like $X=X$.
+
+\item \texttt{trivial with \ident$_1$ \dots\ \ident$_n$}
+
+\item \texttt{trivial with *}
+
+\end{Variants}
+
+\Rem {\tt auto} either solves completely the goal or else leaves it
+intact. \texttt{auto} and \texttt{trivial} never fail.
+
+\SeeAlso Section~\ref{Hints-databases}
+
+\subsection{\tt eauto
+\tacindex{eauto}
+\label{eauto}}
+
+This tactic generalizes {\tt auto}. In contrast with 
+the latter, {\tt eauto} uses unification of the goal
+against the hints rather than pattern-matching
+(in other words, it uses {\tt eapply} instead of
+{\tt apply}).
+As a consequence, {\tt eauto} can solve such a goal:
+
+\begin{coq_example}
+Hint Resolve ex_intro.
+Goal forall P:nat -> Prop, P 0 ->  exists n, P n.
+eauto.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+Note that {\tt ex\_intro} should be declared as an
+hint.
+
+\SeeAlso Section~\ref{Hints-databases}
+
+\subsection{\tt autounfold with  \ident$_1$ \dots\ \ident$_n$
+\tacindex{autounfold}
+\label{autounfold}}
+
+This tactic unfolds constants that were declared through a {\tt Hint
+  Unfold} in the given databases.
+
+\begin{Variants}
+\item {\tt autounfold with \ident$_1$ \dots\ \ident$_n$ in \textit{clause}}
+  
+  Perform the unfolding in the given clause.
+
+\item {\tt autounfold with *}
+  
+  Uses the unfold hints declared in all the hint databases.
+\end{Variants}
+
+
+% EXISTE ENCORE ?
+% 
+% \subsection{\tt Prolog [ \term$_1$ \dots\ \term$_n$ ] \num}
+% \tacindex{Prolog}\label{Prolog}
+% This tactic, implemented by Chet Murthy, is based upon the concept of
+% existential variables of Gilles Dowek, stating that resolution is a
+% kind of unification. It tries to solve the current goal using the {\tt
+%   Assumption} tactic, the {\tt intro} tactic, and applying hypotheses
+% of the local context and terms of the given list {\tt [ \term$_1$
+%   \dots\ \term$_n$\ ]}.  It is more powerful than {\tt auto} since it
+% may apply to any theorem, even those of the form {\tt (x:A)(P x) -> Q}
+% where {\tt x} does not appear free in {\tt Q}.  The maximal search
+% depth is {\tt \num}.
+
+% \begin{ErrMsgs}
+% \item \errindex{Prolog failed}\\
+%   The Prolog tactic was not able to prove the subgoal.
+% \end{ErrMsgs}
+
+\subsection{\tt tauto
+\tacindex{tauto}
+\label{tauto}}
+
+This tactic implements a decision procedure for intuitionistic propositional
+calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
+\cite{Dyc92}. Note that {\tt tauto} succeeds on any instance of an
+intuitionistic tautological proposition. {\tt tauto} unfolds negations
+and logical equivalence but does not unfold any other definition.
+
+The following goal can be proved by {\tt tauto} whereas {\tt auto}
+would fail:
+
+\begin{coq_example}
+Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
+  intros.
+  tauto.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+Moreover, if it has nothing else to do, {\tt tauto} performs
+introductions. Therefore, the use of {\tt intros} in the previous
+proof is unnecessary. {\tt tauto} can for instance prove the
+following:
+\begin{coq_example}
+(* auto would fail *)
+Goal forall (A:Prop) (P:nat -> Prop),
+    A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x.
+
+  tauto.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+\Rem In contrast, {\tt tauto} cannot solve the following goal
+
+\begin{coq_example*}
+Goal forall (A:Prop) (P:nat -> Prop),
+    A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ ~ (A \/ P x).
+\end{coq_example*}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+because \verb=(forall x:nat, ~ A -> P x)= cannot be treated as atomic and an
+instantiation of \verb=x= is necessary.
+
+\subsection{\tt intuition {\tac}
+\tacindex{intuition}
+\label{intuition}}
+
+The tactic \texttt{intuition} takes advantage of the search-tree built
+by the decision procedure involved in the tactic {\tt tauto}. It uses
+this information to generate a set of subgoals equivalent to the
+original one (but simpler than it) and applies the tactic 
+{\tac} to them \cite{Mun94}. If this tactic fails on some goals then
+{\tt intuition} fails. In fact, {\tt tauto} is simply {\tt intuition
+  fail}.
+
+For instance, the tactic {\tt intuition auto} applied to the goal
+\begin{verbatim}
+(forall (x:nat), P x)/\B -> (forall (y:nat),P y)/\ P O \/B/\ P O
+\end{verbatim}
+internally replaces it by the equivalent one:
+\begin{verbatim}
+(forall (x:nat), P x), B |- P O
+\end{verbatim}
+and then uses {\tt auto} which completes the proof.
+
+Originally due to C{\'e}sar~Mu{\~n}oz, these tactics ({\tt tauto} and {\tt intuition})
+have been completely re-engineered by David~Delahaye using mainly the tactic
+language (see Chapter~\ref{TacticLanguage}). The code is now much shorter and
+a significant increase in performance has been noticed. The general behavior
+with respect to dependent types, unfolding and introductions has
+slightly changed to get clearer semantics. This may lead to some
+incompatibilities.
+
+\begin{Variants}
+\item {\tt intuition}\\
+  Is equivalent to {\tt intuition auto with *}.
+\end{Variants}
+
+% 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}}
+
+The tactic \texttt{firstorder} is an {\it experimental} extension of
+\texttt{tauto} to  
+first-order reasoning, written by Pierre Corbineau. 
+It is not restricted to usual logical connectives but
+instead may reason about any first-order class inductive definition.
+
+\begin{Variants}
+ \item {\tt firstorder {\tac}}
+   \tacindex{firstorder {\tac}}
+
+   Tries to solve the goal with {\tac} when no logical rule may apply.
+
+ \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
+   \tacindex{firstorder with}
+
+   Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search
+   environment.
+
+ \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ }
+   \tacindex{firstorder using}
+
+   Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$
+   to the proof-search environment. If {\qualid}$_i$ refers to an inductive
+   type, it is the collection of its constructors which is added as hints.
+
+\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+
+  This combines the effects of the {\tt using} and {\tt with} options.
+
+\end{Variants}
+
+Proof-search is bounded by a depth parameter which can be set by typing the
+{\nobreak \tt Set Firstorder Depth $n$} \comindex{Set Firstorder Depth} 
+vernacular command.
+
+%% \subsection{{\tt jp} {\em (Jprover)}
+%% \tacindex{jp}
+%% \label{jprover}}
+
+%% The tactic \texttt{jp}, due to Huang Guan-Shieng, is an experimental
+%% port of the {\em Jprover}\cite{SLKN01} semi-decision procedure for
+%% first-order intuitionistic logic implemented in {\em
+%%   NuPRL}\cite{Kre02}.
+
+%% The tactic \texttt{jp}, due to Huang Guan-Shieng, is an {\it
+%%   experimental} port of the {\em Jprover}\cite{SLKN01} semi-decision 
+%% procedure for first-order intuitionistic logic implemented in {\em
+%%   NuPRL}\cite{Kre02}. 
+
+%% Search may optionnaly be bounded by a multiplicity parameter
+%% indicating how many (at most) copies of a formula may be used in 
+%% the proof process, its absence may lead to non-termination of the tactic.
+
+%% %\begin{coq_eval}
+%% %Variable S:Set.
+%% %Variables P Q:S->Prop.
+%% %Variable f:S->S.
+%% %\end{coq_eval}
+
+%% %\begin{coq_example*}
+%% %Lemma example: (exists x |P x\/Q x)->(exists x |P x)\/(exists x |Q x).
+%% %jp.
+%% %Qed.
+
+%% %Lemma example2: (forall x ,P x->P (f x))->forall x,P x->P (f(f x)).
+%% %jp.
+%% %Qed.
+%% %\end{coq_example*}
+
+%% \begin{Variants}
+%%  \item {\tt jp $n$}\\
+%%    \tacindex{jp $n$} 
+%%    Tries the {\em Jprover} procedure with multiplicities up to $n$,
+%%    starting from 1.
+%%  \item {\tt jp}\\
+%%    Tries the {\em Jprover} procedure without multiplicity bound, 
+%%    possibly running forever.
+%% \end{Variants}
+
+%% \begin{ErrMsgs}
+%%  \item \errindex{multiplicity limit reached}\\
+%%    The procedure tried all multiplicities below the limit and
+%%    failed. Goal might be solved by increasing the multiplicity limit. 
+%%  \item \errindex{formula is not provable}\\
+%%    The procedure determined that goal was not provable in
+%%    intuitionistic first-order logic, no matter how big the
+%%    multiplicity is.
+%% \end{ErrMsgs}
+
+
+% \subsection[\tt Linear]{\tt Linear\tacindex{Linear}\label{Linear}}
+% The tactic \texttt{Linear}, due to Jean-Christophe Filli{\^a}atre
+% \cite{Fil94}, implements a decision procedure for {\em Direct
+%   Predicate Calculus}, that is first-order Gentzen's Sequent Calculus
+% without contraction rules \cite{KeWe84,BeKe92}.  Intuitively, a
+% first-order goal is provable in Direct Predicate Calculus if it can be
+% proved using each hypothesis at most once.
+
+% Unlike the previous tactics, the \texttt{Linear} tactic does not belong
+% to the initial state of the system, and it must be loaded explicitly
+% with the command
+
+% \begin{coq_example*}
+% Require Linear.
+% \end{coq_example*}
+
+% For instance, assuming that \texttt{even} and \texttt{odd} are two
+% predicates on natural numbers, and \texttt{a} of type \texttt{nat}, the
+% tactic \texttt{Linear} solves the following goal
+
+% \begin{coq_eval}
+% Variables even,odd : nat -> Prop.
+% Variable a:nat.
+% \end{coq_eval}
+
+% \begin{coq_example*}
+% Lemma example : (even a) 
+%               -> ((x:nat)((even x)->(odd (S x))))
+%               -> (EX y | (odd y)).
+% \end{coq_example*}
+
+% You can find examples of the use of \texttt{Linear} in
+% \texttt{theories/DEMOS/DemoLinear.v}.
+% \begin{coq_eval}
+% Abort.
+% \end{coq_eval}
+
+% \begin{Variants}
+% \item {\tt Linear with \ident$_1$ \dots\ \ident$_n$}\\
+%   \tacindex{Linear with} 
+%   Is equivalent to apply first {\tt generalize \ident$_1$ \dots
+%     \ident$_n$} (see Section~\ref{generalize}) then the \texttt{Linear}
+%   tactic.  So one can use axioms, lemmas or hypotheses of the local
+%   context with \texttt{Linear} in this way.
+% \end{Variants}
+
+% \begin{ErrMsgs}
+% \item \errindex{Not provable in Direct Predicate Calculus}
+% \item \errindex{Found $n$ classical proof(s) but no intuitionistic one}\\ 
+%   The decision procedure looks actually for classical proofs of the
+%   goals, and then checks that they are intuitionistic.  In that case,
+%   classical proofs have been found, which do not correspond to
+%   intuitionistic ones.
+% \end{ErrMsgs}
+
+\subsection{\tt congruence
+\tacindex{congruence}
+\label{congruence}}
+
+The tactic {\tt congruence}, by Pierre Corbineau, implements the standard Nelson and Oppen
+congruence closure algorithm, which is a decision procedure for ground
+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. Alternatively, congruence tries to prove that a hypothesis is equal to the goal or to the negation of another hypothesis.
+
+{\tt congruence} is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the members of the equality must contain all the quantified variables in order for {\tt congruence} to match against it. 
+
+\begin{coq_eval}
+Reset Initial.
+Variable A:Set.
+Variables a b:A.
+Variable f:A->A.
+Variable g:A->A->A.
+\end{coq_eval}
+
+\begin{coq_example}
+Theorem T: 
+  a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
+intros.
+congruence.
+\end{coq_example}
+
+\begin{coq_eval}
+Reset Initial.
+Variable A:Set.
+Variables a c d:A.
+Variable f:A->A*A.
+\end{coq_eval}
+
+\begin{coq_example}
+Theorem inj : f = pair a -> Some (f c) = Some (f d) -> c=d.
+intros.
+congruence.
+\end{coq_example}
+
+\begin{Variants}
+ \item {\tt congruence {\sl n}}\\
+  Tries to add at most {\tt \sl n} instances of hypotheses stating quantified equalities to the problem in order to solve it. A bigger value of {\tt \sl n} does not make success slower, only failure. You might consider adding some lemmas as hypotheses using {\tt assert} in order for congruence to use them.
+
+\end{Variants}
+
+\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 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 above.
+\end{ErrMsgs}
+
+\subsection{\tt omega
+\tacindex{omega}
+\label{omega}}
+
+The tactic \texttt{omega}, due to Pierre Cr{\'e}gut,
+is an automatic decision procedure for Presburger
+arithmetic. It solves quantifier-free 
+formulas built with \verb|~|, \verb|\/|, \verb|/\|,
+\verb|->| on top of equalities, inequalities and disequalities on
+both the type \texttt{nat} of natural numbers and \texttt{Z} of binary
+integers. This tactic must be loaded by the command \texttt{Require Import
+  Omega}. See the additional documentation about \texttt{omega}
+(see Chapter~\ref{OmegaChapter}).
+
+\subsection{{\tt ring} and {\tt ring\_simplify \term$_1$ \dots\ \term$_n$}
+\tacindex{ring}
+\tacindex{ring\_simplify}
+\comindex{Add Ring}}
+
+The {\tt ring} tactic solves equations upon polynomial expressions of
+a ring (or semi-ring) structure. It proceeds by normalizing both hand
+sides of the equation (w.r.t. associativity, commutativity and
+distributivity, constant propagation) and comparing syntactically the
+results.
+
+{\tt ring\_simplify} applies the normalization procedure described
+above to the terms given. The tactic then replaces all occurrences of
+the terms given in the conclusion of the goal by their normal
+forms. If no term is given, then the conclusion should be an equation
+and both hand sides are normalized.
+
+See Chapter~\ref{ring} for more information on the tactic and how to
+declare new ring structures.
+
+\subsection{{\tt field}, {\tt field\_simplify \term$_1$\dots\ \term$_n$}
+            and {\tt field\_simplify\_eq}
+\tacindex{field}
+\tacindex{field\_simplify}
+\tacindex{field\_simplify\_eq}
+\comindex{Add Field}}
+
+The {\tt field} tactic is built on the same ideas as {\tt ring}: this
+is a reflexive tactic that solves or simplifies equations in a field
+structure. The main idea is to reduce a field expression (which is an
+extension of ring expressions with the inverse and division
+operations) to a fraction made of two polynomial expressions.
+
+Tactic {\tt field} is used to solve subgoals, whereas {\tt
+  field\_simplify \term$_1$\dots\term$_n$} replaces the provided terms
+by their reduced fraction. {\tt field\_simplify\_eq} applies when the
+conclusion is an equation: it simplifies both hand sides and multiplies
+so as to cancel denominators. So it produces an equation without
+division nor inverse.
+
+All of these 3 tactics may generate a subgoal in order to prove that
+denominators are different from zero.
+
+See Chapter~\ref{ring} for more information on the tactic and how to
+declare new field structures.
+
+\Example
+\begin{coq_example*}
+Require Import Reals.
+Goal forall x y:R,
+    (x * y > 0)%R ->
+    (x * (1 / x + x / (x + y)))%R =
+    ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R.
+\end{coq_example*}
+
+\begin{coq_example}
+intros; field.
+\end{coq_example}
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\SeeAlso file {\tt plugins/setoid\_ring/RealField.v} for an example of instantiation,\\
+\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt
+field}.
+
+\subsection{\tt fourier
+\tacindex{fourier}}
+
+This tactic written by Lo{\"\i}c Pottier solves linear inequalities on
+real numbers using Fourier's method~\cite{Fourier}. This tactic must
+be loaded by {\tt Require Import Fourier}.
+
+\Example
+\begin{coq_example*}
+Require Import Reals.
+Require Import Fourier.
+Goal forall x y:R, (x < y)%R -> (y + 1 >= x - 1)%R.
+\end{coq_example*}
+
+\begin{coq_example}
+intros; fourier.
+\end{coq_example}
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\subsection{\tt autorewrite with \ident$_1$ \dots \ident$_n$.
+\label{tactic:autorewrite}
+\tacindex{autorewrite}}
+
+This tactic \footnote{The behavior of this tactic has much changed compared to
+the versions available in the previous distributions (V6). This may cause
+significant changes in your theories to obtain the same result. As a drawback
+of the re-engineering 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
+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
+the next base is processed. For the bases, the behavior is exactly similar to
+the processing of the rewriting rules.
+
+The rewriting rule bases are built with the {\tt Hint~Rewrite} vernacular
+command.
+
+\Warning{} This tactic may loop if you build non terminating rewriting systems.
+
+\begin{Variant}
+\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 \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
+
+  Performs all the rewritings in hypothesis {\qualid}.
+\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid} using \tac}
+
+  Performs all  the rewritings  in hypothesis {\qualid}  applying {\tt
+    \tac} to the main subgoal after each rewriting step.
+
+\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in \textit{clause}}
+  Performs all  the rewritings  in the clause \textit{clause}. \\
+  The  \textit{clause} argument must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
+
+\end{Variant}
+
+\SeeAlso Section~\ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}.
+
+\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{Controlling automation}
+
+\subsection{The hints databases for {\tt auto} and {\tt eauto}
+\index{Hints databases}
+\label{Hints-databases}
+\comindex{Hint}}
+
+The hints for \texttt{auto} and \texttt{eauto} are stored in
+databases.  Each database maps head symbols to a list of hints. One can
+use the command \texttt{Print Hint \ident} to display the hints
+associated to the head symbol \ident{} (see \ref{PrintHint}). Each
+hint has a cost that is an nonnegative integer, and an optional pattern. 
+The hints with lower cost are tried first. A hint is tried by 
+\texttt{auto} when the conclusion of the current goal
+matches its pattern or when it has no pattern. 
+
+\subsubsection*{Creating Hint databases
+  \label{CreateHintDb}\comindex{CreateHintDb}}
+
+One can optionally declare a hint database using the command
+\texttt{Create HintDb}. If a hint is added to an unknown database, it
+will be automatically created. 
+
+\medskip
+\texttt{Create HintDb} {\ident} [\texttt{discriminated}]
+\medskip
+
+This command creates a new database named \ident.
+The database is implemented by a Discrimination Tree (DT) that serves as
+an index of all the lemmas. The DT can use transparency information to decide
+if a constant should be indexed or not (c.f. \ref{HintTransparency}),
+making the retrieval more efficient.
+The legacy implementation (the default one for new databases) uses the
+DT only on goals without existentials (i.e., auto goals), for non-Immediate
+hints and do not make use of transparency hints, putting more work on the
+unification that is run after retrieval (it keeps a list of the lemmas
+in case the DT is not used). The new implementation enabled by
+the {\tt discriminated} option makes use of DTs in all cases and takes
+transparency information into account. However, the order in which hints
+are retrieved from the DT may differ from the order in which they were
+inserted, making this implementation observationaly different from the
+legacy one. 
+
+\begin{Variants}
+\item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:}
+  \ident$_1$ \ldots\ \ident$_n$
+  
+  This is used to declare a hint database that must not be exported to the other
+  modules that require and import the current module. Inside a
+  section, the option {\tt Local} is useless since hints do not
+  survive anyway to the closure of sections.
+
+\end{Variants}
+
+The general
+command to add a hint to some database \ident$_1$, \dots, \ident$_n$ is:
+\begin{tabbing}
+  \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$
+\end{tabbing}
+where {\sl hint\_definition} is one of the following expressions:
+
+\begin{itemize}
+\item \texttt{Resolve} {\term} 
+  \comindex{Hint Resolve}
+  
+  This command adds {\tt apply {\term}} to the hint list
+  with the head symbol of the type of \term. The cost of that hint is
+  the number of subgoals generated by {\tt apply {\term}}.
+  
+  In case the inferred type of \term\ does not start with a product the
+  tactic added in the hint list is {\tt exact {\term}}. In case this
+  type can be reduced to a type starting with a product, the tactic {\tt
+    apply {\term}} is also stored in the hints list.
+  
+  If the inferred type of \term\ contains a dependent
+  quantification on a predicate, it is added to the hint list of {\tt
+    eapply} instead of the hint list of {\tt apply}. In this case, a
+  warning is printed since the hint is only used by the tactic {\tt
+    eauto} (see \ref{eauto}). A typical example of a hint that is used
+  only by \texttt{eauto} is a transitivity lemma.
+
+  \begin{ErrMsgs}
+  \item \errindex{Bound head variable}
+
+    The head symbol of the type of {\term} is a bound variable such
+    that this tactic cannot be associated to a constant.
+
+  \item \term\ \errindex{cannot be used as a hint}
+
+    The type of \term\ contains products over variables which do not
+    appear in the conclusion. A typical example is a transitivity axiom.
+    In that case the {\tt apply} tactic fails, and thus is useless.
+
+  \end{ErrMsgs}
+
+  \begin{Variants}
+
+  \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$}
+
+    Adds each \texttt{Resolve} {\term$_i$}.
+
+  \end{Variants}
+
+\item \texttt{Immediate {\term}} 
+\comindex{Hint Immediate}
+  
+  This command adds {\tt apply {\term}; trivial} to the hint list
+  associated with the head symbol of the type of {\ident} in the given
+  database. This tactic will fail if all the subgoals generated by
+  {\tt apply {\term}} are not solved immediately by the {\tt trivial}
+  tactic (which only tries tactics with cost $0$).
+  
+  This command is useful for theorems such as the symmetry of equality
+  or $n+1=m+1 \to n=m$ that we may like to introduce with a
+  limited use in order to avoid useless proof-search.
+  
+  The cost of this tactic (which never generates subgoals) is always 1,
+  so that it is not used by {\tt trivial} itself.
+
+  \begin{ErrMsgs}
+
+  \item \errindex{Bound head variable}
+
+  \item \term\ \errindex{cannot be used as a hint} 
+
+  \end{ErrMsgs}
+
+  \begin{Variants}
+
+    \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$} 
+
+      Adds each \texttt{Immediate} {\term$_i$}.
+
+  \end{Variants}
+
+\item \texttt{Constructors} {\ident}
+\comindex{Hint Constructors}
+  
+  If {\ident} is an inductive type, this command adds all its
+  constructors as hints of type \texttt{Resolve}. Then, when the
+  conclusion of current goal has the form \texttt{({\ident} \dots)},
+  \texttt{auto} will try to apply each constructor.
+
+  \begin{ErrMsgs}
+
+    \item {\ident} \errindex{is not an inductive type}
+
+    \item {\ident} \errindex{not declared}
+
+  \end{ErrMsgs}
+
+  \begin{Variants}
+
+    \item \texttt{Constructors} {\ident$_1$} \dots {\ident$_m$} 
+
+      Adds each \texttt{Constructors} {\ident$_i$}.
+
+  \end{Variants}
+
+\item \texttt{Unfold} {\qualid}
+\comindex{Hint Unfold}
+  
+  This adds the tactic {\tt unfold {\qualid}} to the hint list that
+  will only be used when the head constant of the goal is \ident.  Its
+  cost is 4.
+
+  \begin{Variants}
+
+    \item \texttt{Unfold} {\ident$_1$} \dots {\ident$_m$} 
+
+      Adds each \texttt{Unfold} {\ident$_i$}.
+
+  \end{Variants}
+
+\item \texttt{Transparent}, \texttt{Opaque} {\qualid}
+\label{HintTransparency}
+\comindex{Hint Transparent}
+\comindex{Hint Opaque}
+  
+  This adds a transparency hint to the database, making {\tt {\qualid}}
+  a transparent or opaque constant during resolution. This information 
+  is used during unification of the goal with any lemma in the database
+  and inside the discrimination network to relax or constrain it in the
+  case of \texttt{discriminated} databases.
+  
+  \begin{Variants}
+
+    \item \texttt{Transparent}, \texttt{Opaque} {\ident$_1$} \dots {\ident$_m$} 
+
+      Declares each {\ident$_i$} as a transparent or opaque constant.
+      
+  \end{Variants}
+
+\item \texttt{Extern \num\ [\pattern]\ => }\textsl{tactic}
+\comindex{Hint Extern}
+
+  This hint type is to extend \texttt{auto} with tactics other than
+  \texttt{apply} and \texttt{unfold}. For that, we must specify a
+  cost, an optional pattern and a tactic to execute. Here is an example:
+
+\begin{quotation}
+\begin{verbatim}
+Hint Extern 4 ~(?=?) => discriminate.
+\end{verbatim}
+\end{quotation}
+
+  Now, when the head of the goal is a disequality, \texttt{auto} will
+  try \texttt{discriminate} if it does not manage to solve the goal
+  with hints with a cost less than 4.
+  
+  One can even use some sub-patterns of the pattern in the tactic
+  script. A sub-pattern is a question mark followed by an ident, like
+  \texttt{?X1} or \texttt{?X2}. Here is an example:
+
+% Require EqDecide.
+\begin{coq_example*}
+Require Import List.
+\end{coq_example*}
+\begin{coq_example}
+Hint Extern 5   ({?X1 = ?X2} + {?X1 <> ?X2}) =>
+ generalize X1, X2; decide equality : eqdec.
+Goal 
+forall a b:list (nat * nat), {a = b} + {a <> b}.
+info auto with eqdec.
+\end{coq_example}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+\end{itemize}
+
+\Rem One can use an \texttt{Extern} hint with no pattern to do
+pattern-matching on hypotheses using \texttt{match goal with} inside 
+the tactic.
+
+\begin{Variants}
+\item \texttt{Hint} \textsl{hint\_definition} 
+  
+  No database name is given: the hint is registered in the {\tt core} 
+    database. 
+
+\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
+   \ident$_1$ \ldots\ \ident$_n$
+
+  This is used to declare hints that must not be exported to the other
+  modules that require and import the current module. Inside a
+  section, the option {\tt Local} is useless since hints do not
+  survive anyway to the closure of sections.
+
+\item\texttt{Hint Local} \textsl{hint\_definition} 
+
+  Idem for the {\tt core} database.
+    
+\end{Variants}
+
+% There are shortcuts that allow to define several goal at once:
+
+% \begin{itemize}
+% \item \comindex{Hints Resolve}\texttt{Hints Resolve \ident$_1$ \dots\ \ident$_n$ : \ident.}\\
+%   This command is a shortcut for the following ones:
+%   \begin{quotation}
+%    \noindent\texttt{Hint \ident$_1$ : \ident\ := Resolve \ident$_1$}\\
+%    \dots\\
+%    \texttt{Hint \ident$_1$ : \ident := Resolve \ident$_1$}
+%   \end{quotation}
+%   Notice that the hint name is the same that the theorem given as
+%   hint.
+% \item \comindex{Hints Immediate}\texttt{Hints Immediate \ident$_1$ \dots\ \ident$_n$ : \ident.}\\
+% \item \comindex{Hints Unfold}\texttt{Hints Unfold \qualid$_1$ \dots\ \qualid$_n$ : \ident.}\\
+% \end{itemize}
+
+%\begin{Warnings}
+%  \item \texttt{Overriding hint named \dots\ in database \dots}
+%\end{Warnings}
+
+
+
+\subsection{Hint databases defined in the \Coq\ standard library}
+
+Several hint databases are defined in the \Coq\ standard library.  The
+actual content of a database is the collection of the hints declared
+to belong to this database in each of the various modules currently
+loaded.  Especially, requiring new modules potentially extend a
+database. At {\Coq} startup, only the {\tt core} and {\tt v62}
+databases are non empty and can be used.
+
+\begin{description}
+
+\item[\tt core] This special database is automatically used by
+  \texttt{auto}. It contains only basic lemmas about negation,
+  conjunction, and so on from. Most of the hints in this database come 
+  from the \texttt{Init} and \texttt{Logic} directories.
+
+\item[\tt arith] This database contains all lemmas about Peano's
+  arithmetic proved in the directories \texttt{Init} and
+  \texttt{Arith}
+
+\item[\tt zarith] contains lemmas about binary signed integers from
+  the directories \texttt{theories/ZArith}. When required, the module
+  {\tt Omega} also extends the database {\tt zarith} with a high-cost
+  hint that calls {\tt omega} on equations and inequalities in {\tt
+  nat} or {\tt Z}.
+
+\item[\tt bool] contains lemmas about booleans, mostly from directory
+  \texttt{theories/Bool}.
+
+\item[\tt datatypes] is for lemmas about lists, streams and so on that 
+  are mainly proved in the \texttt{Lists} subdirectory.
+
+\item[\tt sets] contains lemmas about sets and relations from the 
+  directories \texttt{Sets} and \texttt{Relations}.
+
+\item[\tt typeclass\_instances] contains all the type class instances
+  declared in the environment, including those used for \texttt{setoid\_rewrite},
+  from the \texttt{Classes} directory.
+\end{description}
+
+There is also a special database called {\tt v62}. It collects all
+hints that were declared in the versions of {\Coq} prior to version
+6.2.4 when the databases {\tt core}, {\tt arith}, and so on were
+introduced.  The purpose of the database {\tt v62} is to ensure
+compatibility with further versions of {\Coq} for developments done in
+versions prior to 6.2.4 ({\tt auto} being replaced by {\tt auto with v62}).
+The database {\tt v62} is intended not to be extended (!). It is not
+included in the hint databases list used in the {\tt auto with *} tactic.
+
+Furthermore, you are advised not to put your own hints in the
+{\tt core} database, but use one or several databases specific to your
+development.
+
+\subsection{\tt Print Hint
+\label{PrintHint}
+\comindex{Print Hint}}
+
+This command displays all hints that apply to the current goal. It
+fails if no proof is being edited, while the two variants can be used at
+every moment.
+
+\begin{Variants}
+
+\item {\tt  Print Hint {\ident} }
+
+ This command displays only tactics associated with \ident\ in the
+ hints list. This is independent of the goal being edited, so this
+ command will not fail if no goal is being edited.
+
+\item {\tt Print Hint *}
+
+  This command displays all declared hints. 
+
+\item {\tt  Print HintDb {\ident} }
+\label{PrintHintDb}
+\comindex{Print HintDb}
+
+ This command displays all hints from database \ident.
+
+\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}}
+
+Hints provided by the \texttt{Hint} commands are erased when closing a
+section. Conversely, all hints of a module \texttt{A} that are not
+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}.]{\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}.]{\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}
+\index{Schemes}
+\comindex{Scheme}}
+
+The {\tt Scheme} command is a high-level tool for generating
+automatically (possibly mutual) induction principles for given types
+and sorts.  Its syntax follows the schema:
+\begin{quote}
+{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
+  with\\
+  \mbox{}\hspace{0.1cm} \dots\\
+        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
+        {\sort$_m$}}
+\end{quote}
+where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type
+identifiers belonging to the same package of mutual inductive
+definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
+to be mutually recursive definitions. Each term {\ident$_i$} proves a
+general principle of mutual induction for objects in type {\term$_i$}.
+
+\begin{Variants}
+\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\
+    with\\
+    \mbox{}\hspace{0.1cm} \dots\ \\
+    with {\ident$_m$} := Minimality for {\ident'$_m$} Sort
+    {\sort$_m$}}
+
+  Same as before but defines a non-dependent elimination principle more
+  natural in case of inductively defined relations. 
+
+\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
+
+  Tries to generate a boolean equality and a proof of the
+  decidability of the usual equality.
+
+\item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
+  with\\
+  \mbox{}\hspace{0.1cm} \dots\\
+        with Induction for {\ident$_m$} Sort
+        {\sort$_m$}}
+
+  If you do not provide the name of the schemes, they will be automatically 
+  computed from the sorts involved (works also with Minimality).
+
+\end{Variants}
+
+\SeeAlso Section~\ref{Scheme-examples}
+
+\subsection{Automatic declaration of schemes}
+\comindex{Set Equality Schemes}
+\comindex{Set Elimination Schemes}
+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}. 
+\\
+
+You can also activate the automatic declaration of those boolean equalities 
+(see the second variant of {\tt Scheme})  with the {\tt Set Equality Schemes}
+ 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.
+
+\subsection{\tt Combined Scheme\label{CombinedScheme}
+\comindex{Combined Scheme}}
+The {\tt Combined Scheme} command is a tool for combining 
+induction principles generated by the {\tt Scheme} command.
+Its syntax follows the schema :
+
+\noindent
+{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\
+\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
+the same package of mutual inductive principle definitions. This command
+generates {\ident$_0$} to be the conjunction of the principles: it is
+built from the common premises of the principles and concluded by the
+conjunction of their conclusions.
+
+\SeeAlso Section~\ref{CombinedScheme-examples}
+
+\section{Generation of induction principles with {\tt Functional Scheme}
+\label{FunScheme}
+\comindex{Functional Scheme}}
+
+The {\tt Functional Scheme} command is a high-level experimental
+tool for generating automatically induction principles
+corresponding to (possibly mutually recursive) functions.  Its
+syntax follows the schema:
+\begin{quote}
+{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
+  with\\
+  \mbox{}\hspace{0.1cm} \dots\ \\
+        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
+        {\sort$_m$}}
+\end{quote}  
+where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
+names (they must be in the same order as when they were defined).
+This command generates the induction principles
+\ident$_1$\dots\ident$_m$, following the recursive structure and case
+analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
+
+
+\paragraph{\texttt{Functional Scheme}} 
+There is a difference between obtaining an induction scheme by using
+\texttt{Functional Scheme} on a function defined by \texttt{Function}
+or not. Indeed \texttt{Function} generally produces smaller
+principles, closer to the definition written by the user.
+
+
+\SeeAlso Section~\ref{FunScheme-examples}
+
+
+\section{Simple tactic macros
+\index{Tactic macros}
+\comindex{Tactic Definition}
+\label{TacticDefinition}}
+
+A simple example has more value than a long explanation: 
+
+\begin{coq_example}
+Ltac Solve := simpl; intros; auto.
+Ltac ElimBoolRewrite b H1 H2 :=
+  elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ].
+\end{coq_example}
+
+The tactics macros are synchronous with the \Coq\ section mechanism:
+a tactic definition is deleted from the current environment
+when you close the section (see also \ref{Section}) 
+where it was defined. If you want that a
+tactic macro defined in a module is usable in the modules that
+require it, you should put it outside of any section.
+
+Chapter~\ref{TacticLanguage} gives examples of more complex
+user-defined tactics.
+
+
+% $Id: RefMan-tac.tex 13344 2010-07-28 15:04:36Z msozeau $ 
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% TeX-master: "Reference-Manual"
+%%% End: