Mercurial > cpdt > repo

comparison src/Tactics.v @ 204:cbf2f74a5130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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