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 | b3bfa064636a8507e0fe83779791dbbee6f15c38 (patch) | |
tree | 6fb9724c03715a330a6ee10a1e9b09340e1f6d0b /src | |
parent | 18c2f489867bf282c49346eb090b22e41ec5f67a (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 |