Mercurial > cpdt > repo
diff src/Tactics.v @ 99:8c7d9b82a4a4
crush' pursues trivial inversions
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 08 Oct 2008 09:41:50 -0400 |
| parents | cde1351d18bb |
| children | ee676bf3d681 |
line wrap: on
line diff
--- a/src/Tactics.v Tue Oct 07 22:14:39 2008 -0400 +++ b/src/Tactics.v Wed Oct 08 09:41:50 2008 -0400 @@ -42,6 +42,9 @@ end. Ltac simplHyp invOne := + let invert H F := + inList F invOne; (inversion H; fail) + || (inversion H; [idtac]; clear H; try subst) in match goal with | [ H : ex _ |- _ ] => destruct H @@ -54,11 +57,11 @@ | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst end - | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst - | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst - | [ H : ?F _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst - | [ H : ?F _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst - | [ H : ?F _ _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst + | [ H : ?F _ |- _ ] => invert H F + | [ H : ?F _ _ |- _ ] => invert H F + | [ H : ?F _ _ _ |- _ ] => invert H F + | [ H : ?F _ _ _ _ |- _ ] => invert H F + | [ H : ?F _ _ _ _ _ |- _ ] => invert H F end. Ltac rewriteHyp :=