Mercurial > cpdt > repo

diff src/Coinductive.v @ 65:21bb59c56b98

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove [done] markers after enhancement phase finishes
author Adam Chlipala <adamc@hcoop.net>
date Wed, 01 Oct 2008 09:32:36 -0400
parents 739c2818d6e2
children 55199444e5e7
line wrap: on
line diff
--- 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.