Mercurial > cpdt > repo
comparison src/Tactics.v @ 204:cbf2f74a5130
Parts I want to keep compile with 8.2
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 06 Nov 2009 10:52:43 -0500 |
parents | df289eb8ef76 |
children | c4b1c0de7af9 |
comparison
equal
deleted
inserted
replaced
203:71ade09024ac | 204:cbf2f74a5130 |
---|---|
46 inList F invOne; (inversion H; fail) | 46 inList F invOne; (inversion H; fail) |
47 || (inversion H; [idtac]; clear H; try subst) in | 47 || (inversion H; [idtac]; clear H; try subst) in |
48 match goal with | 48 match goal with |
49 | [ H : ex _ |- _ ] => destruct H | 49 | [ H : ex _ |- _ ] => destruct H |
50 | 50 |
51 | [ H : ?F ?X = ?F ?Y |- _ ] => injection H; | 51 | [ H : ?F ?X = ?F ?Y |- ?G ] => |
52 match goal with | 52 (assert (X = Y); [ assumption | fail 1 ]) |
53 | [ |- F X = F Y -> _ ] => fail 1 | 53 || (injection H; |
54 | [ |- _ = _ -> _ ] => try clear H; intros; try subst | 54 match goal with |
55 end | 55 | [ |- X = Y -> G ] => |
56 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H; | 56 try clear H; intros; try subst |
57 match goal with | 57 end) |
58 | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst | 58 | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] => |
59 end | 59 (assert (X = Y); [ assumption |
60 | assert (U = V); [ assumption | fail 1 ] ]) | |
61 || (injection H; | |
62 match goal with | |
63 | [ |- U = V -> X = Y -> G ] => | |
64 try clear H; intros; try subst | |
65 end) | |
60 | 66 |
61 | [ H : ?F _ |- _ ] => invert H F | 67 | [ H : ?F _ |- _ ] => invert H F |
62 | [ H : ?F _ _ |- _ ] => invert H F | 68 | [ H : ?F _ _ |- _ ] => invert H F |
63 | [ H : ?F _ _ _ |- _ ] => invert H F | 69 | [ H : ?F _ _ _ |- _ ] => invert H F |
64 | [ H : ?F _ _ _ _ |- _ ] => invert H F | 70 | [ H : ?F _ _ _ _ |- _ ] => invert H F |