--- a/src/Coinductive.v	Mon Oct 06 14:41:13 2008 -0400
+++ b/src/Coinductive.v	Tue Oct 07 10:43:54 2008 -0400
@@ -412,7 +412,7 @@
 (** remove printing * *)
 Ltac compat := unfold regmapCompat in *; crush;
   match goal with
-    | [ |- match get _ ?R with Some _ => _ | None => _ end ] => destruct R; crush
+    | [ H : _ |- match get _ ?R with Some _ => _ | None => _ end ] => generalize (H R); destruct R; crush
   end.
 
 Lemma regmapCompat_set_None : forall rm rm' r n,

--- a/src/Tactics.v	Mon Oct 06 14:41:13 2008 -0400
+++ b/src/Tactics.v	Tue Oct 07 10:43:54 2008 -0400
@@ -111,17 +111,16 @@
            | [ H : done _ |- _ ] => clear H
          end.
 
-Ltac crush'' tryLemmas lemmas invOne :=
+Ltac crush' lemmas invOne :=
   let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence
     in (sintuition; rewriter;
-      match tryLemmas with
-        | true => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
+      match lemmas with
+        | false => idtac
+        | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
           repeat (simplHyp invOne; intuition)); un_done
-        | _ => idtac
       end; sintuition; try omega; try (elimtype False; omega)).
 
-Ltac crush := crush'' false tt fail.
-Ltac crush' := crush'' true.
+Ltac crush := crush' false fail.
 
 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
   (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with