Merge branch 'v8.5'

1 files changed, 24 insertions, 31 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b855a0eacc..ddb48b0c1b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1531,25 +1531,27 @@ for each possible form of {\term}, i.e. one for each constructor of
 the inductive or co-inductive type. Unlike {\tt induction}, no
 induction hypothesis is generated by {\tt destruct}.
 
-If the argument is dependent in either the conclusion or some
-hypotheses of the goal, the argument is replaced by the appropriate
-constructor form in each of the resulting subgoals, thus performing
-case analysis. If non-dependent, the tactic simply exposes the
-inductive or co-inductive structure of the argument.
-
 There are special 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}}.
+  variable of the conclusion of the goal, then {\tt destruct {\ident}}
+  behaves as {\tt intros until {\ident}; destruct {\ident}}. If
+  {\ident} is not anymore dependent in the goal after application of
+  {\tt destruct}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt 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. Remark: For destruction of a numeral, use
 syntax {\tt destruct ({\num})} (not very interesting anyway).
 
+\item In case {\term} is an hypothesis {\ident} of the context,
+  and {\ident} is not anymore dependent in the goal after
+  application of {\tt destruct}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt destruct ({\ident})}).
+
 \item The argument {\term} can also be a pattern of which holes are
   denoted by ``\_''. In this case, the tactic checks that all subterms
   matching the pattern in the conclusion and the hypotheses are
@@ -1626,14 +1628,6 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using},
   and {\tt in} clauses.
 
-\item{\tt destruct !{\ident}}
-
-  This is a case when the destructed term is an hypothesis of the
-  context. The ``!'' modifier tells to keep the hypothesis in the
-  context after destruction.
-
-  This applies also to the other form of {\tt destruct} and {\tt edestruct}.
-
 \item{\tt case \term}\label{case}\tacindex{case}
 
   The tactic {\tt case} is a more basic tactic to perform case
@@ -1699,14 +1693,22 @@ 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}}.
+  variable of the conclusion of the goal, then {\tt induction
+    {\ident}} behaves as {\tt intros until {\ident}; induction
+    {\ident}}.  If {\ident} is not anymore dependent in the goal
+  after application of {\tt induction}, it is erased (to avoid
+  erasure, use parentheses, as in {\tt 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. Remark: For simple induction on a numeral,
 use syntax {\tt induction ({\num})} (not very interesting anyway).
 
+\item In case {\term} is an hypothesis {\ident} of the context,
+  and {\ident} is not anymore dependent in the goal after
+  application of {\tt induction}, it is erased (to avoid erasure, use
+  parentheses, as in {\tt induction ({\ident})}).
+
 \item The argument {\term} can also be a pattern of which holes are
   denoted by ``\_''. In this case, the tactic checks that all subterms
   matching the pattern in the conclusion and the hypotheses are
@@ -1821,15 +1823,6 @@ Show 2.
   einduction}.  It combines the effects of the {\tt with}, {\tt as}, %%{\tt eqn:},
   {\tt using}, and {\tt in} clauses.
 
-\item{\tt induction !{\ident}}
-
-  This is a case when the term on which to apply induction is an
-  hypothesis of the context. The ``!'' modifier tells to keep the
-  hypothesis in the context after induction.
-
-  This applies also to the other form of {\tt induction} and {\tt
-    einduction}.
-
 \item {\tt elim \term}\label{elim}
 
   This is a more basic induction tactic.  Again, the type of the
@@ -3562,7 +3555,7 @@ 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.
+hint has a cost that is a 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.
@@ -3779,7 +3772,7 @@ Hint Extern 4 (~(_ = _)) => discriminate.
   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
+  script. A sub-pattern is a question mark followed by an identifier, like
   \texttt{?X1} or \texttt{?X2}. Here is an example:
 
 % Require EqDecide.
@@ -3822,7 +3815,7 @@ The \texttt{emp} regexp does not match any search path while
 \texttt{eps} matches the empty path. During proof search, the path of
 successive successful hints on a search branch is recorded, as a list of
 identifiers for the hints (note \texttt{Hint Extern}'s do not have an
-associated identitier). Before applying any hint $\ident$ the current
+associated identifier). Before applying any hint $\ident$ the current
 path $p$ extended with $\ident$ is matched against the current cut
 expression $c$ associated to the hint database. If matching succeeds,
 the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$
@@ -4679,7 +4672,7 @@ Use \texttt{classical\_right} to prove the right part of the disjunction with th
 %% procedure for first-order intuitionistic logic implemented in {\em
 %%   NuPRL}\cite{Kre02}.
 
-%% Search may optionnaly be bounded by a multiplicity parameter
+%% Search may optionally 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.