# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223473310 14400
# Node ID 8c7d9b82a4a44e4ec44acfed9edee0f36f0123df
# Parent  696726af9530c767fbaa1fd78b8a38a0faca7a30
crush' pursues trivial inversions

diff -r 696726af9530 -r 8c7d9b82a4a4 src/Tactics.v
--- 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 :=