Mercurial > cpdt > repo

comparison src/Tactics.v @ 84:522436ed6688

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