summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-03-10 13:46:45 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-03-10 13:46:45 -0400
commitb3bfa064636a8507e0fe83779791dbbee6f15c38 (patch)
tree6fb9724c03715a330a6ee10a1e9b09340e1f6d0b /src
parent18c2f489867bf282c49346eb090b22e41ec5f67a (diff)
Prose for ListEdit
Diffstat (limited to 'src')
-rw-r--r--src/elaborate.sml17
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