dependent destruction: Fix (part of) bug #3961, by fixing dependent *

generalizing * which was broken since 8.4.

1 files changed, 13 insertions, 5 deletions

diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 668a68c9c7..9f4ddc8044 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -247,7 +247,7 @@ to simplify equalities appearing at the beginning of induction
 hypotheses, generally using trivial applications of
 reflexivity. In cases where the equality is not between constructor
 forms though, one must help the automation by giving
-some arguments, using the {\tt specialize} tactic.
+some arguments, using the {\tt specialize} tactic for example.
 
 \begin{coq_example*}
 destruct D... apply weak ; apply ax. apply ax.
@@ -257,16 +257,24 @@ destruct D...
 Show.
 \end{coq_example}
 \begin{coq_example}
-  specialize (IHterm G empty).
+  specialize (IHterm G0 empty eq_refl).
 \end{coq_example}
 
-Then the automation can find the needed equality {\tt G = G} to narrow
-the induction hypothesis further. This concludes our example.
+Once the induction hypothesis has been narrowed to the right equality,
+it can be used directly. 
 
 \begin{coq_example}
-  simpl_depind.
+  apply weak, IHterm.
 \end{coq_example}
 
+If there is an easy first-order solution to these equations as in this subgoal, the
+{\tt specialize\_eqs} tactic can be used instead of giving explicit proof
+terms:
+
+\begin{coq_example}
+  specialize_eqs IHterm.
+\end{coq_example}
+This concludes our example.
 \SeeAlso The induction \ref{elim}, case \ref{case} and inversion \ref{inversion} tactics.
 
 \section[\tt autorewrite]{\tt autorewrite\label{autorewrite-example}}