# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1222867956 14400
# Node ID 21bb59c56b9851fe964960cc9e6f02d8551241cd
# Parent  739c2818d6e2e38d60f6caac94c126aa78f10b4d
Remove [done] markers after enhancement phase finishes

diff -r 739c2818d6e2 -r 21bb59c56b98 src/Coinductive.v
--- a/src/Coinductive.v	Tue Sep 30 17:47:59 2008 -0400
+++ b/src/Coinductive.v	Wed Oct 01 09:32:36 2008 -0400
@@ -413,12 +413,12 @@
     Hint Resolve regmapCompat_set_None regmapCompat_set_Some.
     Hint Constructors run.
 
-    cofix.
-    destruct 1; crush; eauto;
-      repeat match goal with
-               | [ H : regmapCompat _ _ |- run _ _ (match get ?RM ?R with Some _ => _ | None => _ end) _ ] =>
-                 generalize (H R); destruct (get RM R); crush
-             end.
+    cofix;
+      destruct 1; crush; eauto;
+        repeat match goal with
+                 | [ H : regmapCompat _ _ |- run _ _ (match get ?RM ?R with Some _ => _ | None => _ end) _ ] =>
+                   generalize (H R); destruct (get RM R); crush
+               end.
   Qed.
 End constFold_ok.
 
diff -r 739c2818d6e2 -r 21bb59c56b98 src/Tactics.v
--- a/src/Tactics.v	Tue Sep 30 17:47:59 2008 -0400
+++ b/src/Tactics.v	Wed Oct 01 09:32:36 2008 -0400
@@ -102,11 +102,16 @@
       end
   end.
 
+Ltac un_done :=
+  repeat match goal with
+           | [ H : done _ |- _ ] => clear H
+         end.
+
 Ltac crush' lemmas invOne :=
   let sintuition := simpl in *; intuition; subst; repeat (simplHyp invOne; intuition; 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));
-      sintuition; try omega).
+      un_done; sintuition; try omega).
 
 Ltac crush := crush' tt fail.