Mercurial > cpdt > repo

changeset 66:b52204928c7d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Put [try] in front of [subst], to avoid whining about recursive equalities
author Adam Chlipala <adamc@hcoop.net>
date Wed, 01 Oct 2008 09:33:44 -0400
parents 21bb59c56b98
children 55199444e5e7
files src/Tactics.v
diffstat 1 files changed, 6 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- 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));