Mercurial > cpdt > repo
comparison src/Tactics.v @ 179:8f3fc56b90d4
PatMatch Elaborate_correct
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 10 Nov 2008 14:12:22 -0500 |
parents | 9b1f58dbc464 |
children | 02569049397b |
comparison
equal
deleted
inserted
replaced
178:f41d4e43fd30 | 179:8f3fc56b90d4 |
---|---|
64 | [ H : ?F _ _ _ _ |- _ ] => invert H F | 64 | [ H : ?F _ _ _ _ |- _ ] => invert H F |
65 | [ H : ?F _ _ _ _ _ |- _ ] => invert H F | 65 | [ H : ?F _ _ _ _ _ |- _ ] => invert H F |
66 | 66 |
67 | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H | 67 | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H |
68 | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H | 68 | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H |
69 | |
70 | [ H : Some _ = Some _ |- _ ] => injection H; clear H | |
69 end. | 71 end. |
70 | 72 |
71 Ltac rewriteHyp := | 73 Ltac rewriteHyp := |
72 match goal with | 74 match goal with |
73 | [ H : _ |- _ ] => rewrite H | 75 | [ H : _ |- _ ] => rewrite H |