Improve the dependent induction tactic to automatically find the

generalized hypotheses. Also move part of the tactic to ML and
improve the generated proof term in case of non-dependent induction.


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

1 files changed, 8 insertions, 11 deletions

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index b56ca26c3..bb1ffbd2b 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -231,37 +231,34 @@ Ltac simpl_depind := subst* ; autoinjections ; try discriminates ;
    by first generalizing it and adding the proper equalities to the context, in a maner similar to 
    the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
 
-(** First a tactic to prepare for a dependent induction on an hypothesis [H]. *)
-
-Ltac prepare_depind H :=
-  let oldH := fresh "old" H in
-    generalize_eqs H ; rename H into oldH ; (intros until H || intros until 1) ; 
-      generalize dependent oldH ;
-        try (intros _ _) (* If the goal is not dependent on the hyp, we can prove a stronger statement *).
-
 (** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis 
    and starts a dependent induction using this tactic. *)
 
 Ltac do_depind tac H :=
-  prepare_depind H ; tac H ; repeat progress simpl_depind.
+  generalize_eqs H ; tac H ; repeat progress simpl_depind.
 
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *)
 
 Tactic Notation "dependent" "destruction" ident(H) := 
   do_depind ltac:(fun H => destruct H ; intros) H ; subst*.
 
+Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
+  do_depind ltac:(fun H => destruct H using c ; intros) H.
+
 (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
    writting another wrapper calling do_depind. *)
 
 Tactic Notation "dependent" "induction" ident(H) := 
   do_depind ltac:(fun H => induction H ; intros) H.
 
+Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
+  do_depind ltac:(fun H => induction H using c ; intros) H.
+
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
   do_depind ltac:(fun H => generalize l ; clear l ; induction H ; intros) H.
 
-(** This tactic also generalizes the goal by the given variables before the induction. *)
-
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
   do_depind ltac:(fun H => generalize l ; clear l ; induction H using c ; intros) H.
+