Fixes in generalize_eqs/dependent induction to allow the user to specify

generalized variables himself.


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

2 files changed, 23 insertions, 18 deletions

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 89e44c9bc..cd30d77ca 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -235,30 +235,43 @@ Ltac simpl_depind := subst* ; autoinjections ; try discriminates ;
    and starts a dependent induction using this tactic. *)
 
 Ltac do_depind tac H :=
+  generalize_eqs_vars H ; tac H ; repeat progress simpl_depind.
+
+(** A variant where generalized variables should be given by the user. *)
+
+Ltac do_depind' tac H :=
   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*.
+  do_depind ltac:(fun hyp => destruct hyp ; intros) H ; subst*.
 
 Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
-  do_depind ltac:(fun H => destruct H using c ; intros) H.
+  do_depind ltac:(fun hyp => destruct hyp using c ; intros) H.
+
+(** This tactic also generalizes the goal by the given variables before the induction. *)
+
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
+  do_depind' ltac:(fun hyp => revert l ; destruct hyp ; intros) H.
+
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+  do_depind' ltac:(fun hyp => revert l ; destruct hyp 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.
+  do_depind ltac:(fun hyp => induction hyp ; intros) H.
 
 Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
-  do_depind ltac:(fun H => induction H using c ; intros) H.
+  do_depind ltac:(fun hyp => induction hyp 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.
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp ; intros) H.
 
 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.
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c ; intros) H.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 45e965142..d7535c323 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -77,10 +77,10 @@ Ltac clear_dup :=
   match goal with 
     | [ H : ?X |- _ ] => 
       match goal with
-        | [ H' : X |- _ ] =>
-          match H' with
-            | H => fail 2 
-            | _ => clear H' || clear H
+        | [ H' : ?Y |- _ ] =>
+          match H with
+            | H' => fail 2
+            | _ => conv X Y ; (clear H' || clear H)
           end
       end
   end.
@@ -158,14 +158,6 @@ Ltac autoinjection :=
   let tac H := progress (inversion H ; subst ; clear_dups) ; clear H in
     match goal with
       | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
-      | [ H : ?f ?a ?b = ?f' ?a' ?b'  |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g'  |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
     end.
 
 Ltac autoinjections := repeat autoinjection.