Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/Tactics.v Sun Jan 04 08:18:59 2009 -0500 +++ b/src/Tactics.v Fri Nov 06 10:52:43 2009 -0500 @@ -48,15 +48,21 @@ match goal with | [ H : ex _ |- _ ] => destruct H - | [ H : ?F ?X = ?F ?Y |- _ ] => injection H; - match goal with - | [ |- F X = F Y -> _ ] => fail 1 - | [ |- _ = _ -> _ ] => try clear H; intros; try subst - end - | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H; - match goal with - | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst - end + | [ H : ?F ?X = ?F ?Y |- ?G ] => + (assert (X = Y); [ assumption | fail 1 ]) + || (injection H; + match goal with + | [ |- X = Y -> G ] => + try clear H; intros; try subst + end) + | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] => + (assert (X = Y); [ assumption + | assert (U = V); [ assumption | fail 1 ] ]) + || (injection H; + match goal with + | [ |- U = V -> X = Y -> G ] => + try clear H; intros; try subst + end) | [ H : ?F _ |- _ ] => invert H F | [ H : ?F _ _ |- _ ] => invert H F