Mercurial > cpdt > repo

diff src/Coinductive.v @ 88:cde1351d18bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Get Coinductive compiling again
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 10:43:54 -0400
parents f295a64bf9fd
children 32a5ad6e2bb0
line wrap: on
line diff
--- 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,