Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/Tactics.v Mon Nov 10 12:19:47 2008 -0500 +++ b/src/Tactics.v Mon Nov 10 14:12:22 2008 -0500 @@ -66,6 +66,8 @@ | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H + + | [ H : Some _ = Some _ |- _ ] => injection H; clear H end. Ltac rewriteHyp :=