# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223390634 14400
# Node ID cde1351d18bb8d8b8bcef02a1077494f429ffca6
# Parent  a0b8b550e265c5a3abc4e6c9c4d2183b72c781d1
Get Coinductive compiling again

diff -r a0b8b550e265 -r cde1351d18bb src/Coinductive.v
--- 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,
diff -r a0b8b550e265 -r cde1351d18bb src/Tactics.v
--- 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