diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-28 09:24:15 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-28 09:24:15 +0000 |
| commit | f7665a72dba3a896997220d738597cfe05b27990 (patch) | |
| tree | 9bf47da71e2a912832199c6d13633d8ddee34678 /theories/Program/Tactics.v | |
| parent | 059a0622a512e40ffc1944cdc6084c3462aa85f9 (diff) | |
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
Diffstat (limited to 'theories/Program/Tactics.v')
| -rw-r--r-- | theories/Program/Tactics.v | 16 |
1 files changed, 4 insertions, 12 deletions
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. |