Fixes in dependent induction tactic to keep names, allow giving

intro-patterns and avoid useless generalizations on inductive 
parameters.


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

1 files changed, 9 insertions, 7 deletions

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index d7535c323..49b883342 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -91,7 +91,7 @@ Ltac clear_dups := repeat clear_dup.
 
 Ltac subst_no_fail :=
   repeat (match goal with 
-            [ H : ?X = ?Y |- _ ] => subst X || subst Y                  
+            [ H : ?X = ?Y |- _ ] => subst X || subst Y
           end).
 
 Tactic Notation "subst" "*" := subst_no_fail.
@@ -154,13 +154,15 @@ Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(i
 
 (** Try to inject any potential constructor equality hypothesis. *)
 
-Ltac autoinjection :=
-  let tac H := progress (inversion H ; subst ; clear_dups) ; clear H in
-    match goal with
-      | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
-    end.
+Ltac autoinjection tac :=
+  match goal with
+    | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
+  end.
+
+Ltac inject H :=
+  progress (inversion H ; subst* ; clear_dups) ; clear H.
 
-Ltac autoinjections := repeat autoinjection.
+Ltac autoinjections := repeat autoinjection ltac:inject.
 
 (** Destruct an hypothesis by first copying it to avoid dependencies. *)