# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1222868024 14400
# Node ID b52204928c7d912a569c9a7a3eb1793985cdd790
# Parent  21bb59c56b9851fe964960cc9e6f02d8551241cd
Put [try] in front of [subst], to avoid whining about recursive equalities

diff -r 21bb59c56b98 -r b52204928c7d src/Tactics.v
--- a/src/Tactics.v	Wed Oct 01 09:32:36 2008 -0400
+++ b/src/Tactics.v	Wed Oct 01 09:33:44 2008 -0400
@@ -14,7 +14,7 @@
 Set Implicit Arguments.
 
 
-Ltac inject H := injection H; clear H; intros; subst.
+Ltac inject H := injection H; clear H; intros; try subst.
 
 Ltac appHyps f :=
   match goal with
@@ -46,15 +46,15 @@
 
     | [ H : ?F _ = ?F _ |- _ ] => injection H;
       match goal with
-        | [ |- _ = _ -> _ ] => clear H; intros; subst
+        | [ |- _ = _ -> _ ] => clear H; intros; try subst
       end
     | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
       match goal with
-        | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst
+        | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; try subst
       end
 
-    | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst
-    | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; 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
   end.
 
 Ltac rewriteHyp :=
@@ -108,7 +108,7 @@
          end.
 
 Ltac crush' lemmas invOne :=
-  let sintuition := simpl in *; intuition; subst; repeat (simplHyp invOne; intuition; subst); try congruence
+  let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence
     in (sintuition; rewriter;
       repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
         repeat (simplHyp invOne; intuition));