diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-03-10 13:46:45 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-03-10 13:46:45 -0400 |
commit | 8d6dd2b06eb70e446048b50d5995d38fd9de63f9 (patch) | |
tree | 6fb9724c03715a330a6ee10a1e9b09340e1f6d0b /src | |
parent | e2bfa72019653e309b7cdc3cf4ce4e6153712b1b (diff) |
Prose for ListEdit
Diffstat (limited to 'src')
-rw-r--r-- | src/elaborate.sml | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 5e94d8e4..daa6e004 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -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 |