diff src/elaborate.sml @ 647:ae374df5ccbd

Prose for ListEdit
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Mar 2009 13:46:45 -0400
parents fb2a0e76dcef
children fab5998b840e
line wrap: on
line diff
--- a/src/elaborate.sml	Tue Mar 10 12:44:40 2009 -0400
+++ b/src/elaborate.sml	Tue Mar 10 13:46:45 2009 -0400
@@ -706,13 +706,6 @@
                                           ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
 
          val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
-         fun eatMost unifs =
-             case unifs of
-                 (_, r) :: (rest as _ :: _) => (r := SOME (L'.CRecord (k, []), loc);
-                                                eatMost rest)
-               | _ => unifs
-         val unifs1 = eatMost unifs1
-         val unifs2 = eatMost unifs2
 
          val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2)
          (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
@@ -887,6 +880,11 @@
              (L'.CError, _) => ()
            | (_, L'.CError) => ()
 
+           | (L'.CRecord _, _) => isRecord ()
+           | (_, L'.CRecord _) => isRecord ()
+           | (L'.CConcat _, _) => isRecord ()
+           | (_, L'.CConcat _) => isRecord ()
+
            | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
              if r1 = r2 then
                  ()
@@ -1034,11 +1032,6 @@
            | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
              unifyCons' (E.pushKRel env x) c1 c2
 
-           | (L'.CRecord _, _) => isRecord ()
-           | (_, L'.CRecord _) => isRecord ()
-           | (L'.CConcat _, _) => isRecord ()
-           | (_, L'.CConcat _) => isRecord ()
-
            | _ => err CIncompatible
      end