Mercurial > cpdt > repo

changeset 99:8c7d9b82a4a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
crush' pursues trivial inversions
author Adam Chlipala <adamc@hcoop.net>
date Wed, 08 Oct 2008 09:41:50 -0400
parents 696726af9530
children 070f4de92311
files src/Tactics.v
diffstat 1 files changed, 8 insertions(+), 5 deletions(-) [+]
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 :=