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

generalizing * which was broken since 8.4.

2 files changed, 22 insertions, 7 deletions

diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 668a68c9c..9f4ddc804 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}}
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index a9aa30df5..ae6fe7dd0 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -426,8 +426,9 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.
 (** A variant where generalized variables should be given by the user. *)
 
 Ltac do_depelim' rev tac H :=
-  (try intros until H) ; block_goal ; rev H ;
-  (try revert_until H ; block_goal) ; generalize_eqs H ; tac H ; simpl_dep_elim.
+  (try intros until H) ; block_goal ; 
+  (try revert_until H ; block_goal) ; 
+  generalize_eqs H ; rev H ; tac H ; simpl_dep_elim.
 
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
    By default, we don't try to generalize the hyp by its variable indices.  *)
@@ -463,3 +464,9 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H.
+
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) :=
+  do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l) H.
+
+Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) "using" constr(c) := 
+  do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l using c) H.