Mercurial > cpdt > repo
comparison src/Tactics.v @ 84:522436ed6688
Incorporate crush' bug reports; ilists in MoreDep
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 05 Oct 2008 20:07:35 -0400 |
parents | 506a06118014 |
children | 3746a2ded8da |
comparison
equal
deleted
inserted
replaced
83:d992227e4814 | 84:522436ed6688 |
---|---|
22 end. | 22 end. |
23 | 23 |
24 Ltac inList x ls := | 24 Ltac inList x ls := |
25 match ls with | 25 match ls with |
26 | x => idtac | 26 | x => idtac |
27 | (_, x) => idtac | |
27 | (?LS, _) => inList x LS | 28 | (?LS, _) => inList x LS |
28 end. | 29 end. |
29 | 30 |
30 Ltac app f ls := | 31 Ltac app f ls := |
31 match ls with | 32 match ls with |
53 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; try subst | 54 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; try subst |
54 end | 55 end |
55 | 56 |
56 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst | 57 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst |
57 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst | 58 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst |
59 | [ H : ?F _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst | |
60 | [ H : ?F _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst | |
61 | [ H : ?F _ _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst | |
58 end. | 62 end. |
59 | 63 |
60 Ltac rewriteHyp := | 64 Ltac rewriteHyp := |
61 match goal with | 65 match goal with |
62 | [ H : _ |- _ ] => rewrite H | 66 | [ H : _ |- _ ] => rewrite H |