diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-21 15:53:17 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-21 15:53:17 +0000 |
commit | bc0fc3752b85e7f1c71b2f049ed8c8e006fca9c7 (patch) | |
tree | 1021fd81bde7405296e8cbd0afc8e29cae302361 /theories/Program/Tactics.v | |
parent | 70aa6184a399ebf2b70bf284ad57fc4e4dd5c226 (diff) |
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
Diffstat (limited to 'theories/Program/Tactics.v')
-rw-r--r-- | theories/Program/Tactics.v | 16 |
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. *) |