summaryrefslogtreecommitdiff
path: root/src/explify.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 12:25:12 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-01 12:25:12 -0400
commitf7d2bdce780d0333431829a8a788bdb208c0dcbc (patch)
tree5316084519f313741563c016ac6733d03f892475 /src/explify.sml
parent7628e1d8f7f8199531c9bc08a774c9a9e2bc5d63 (diff)
Disjointness assumptions in expressions
Diffstat (limited to 'src/explify.sml')
-rw-r--r--src/explify.sml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/explify.sml b/src/explify.sml
index 2ed66843..0fa3698b 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -48,6 +48,7 @@ fun explifyCon (c, loc) =
case c of
L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
| L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc)
+ | L.TDisjoint (_, _, c) => explifyCon c
| L.TRecord c => (L'.TRecord (explifyCon c), loc)
| L.CRel n => (L'.CRel n, loc)
@@ -56,7 +57,7 @@ fun explifyCon (c, loc) =
| L.CApp (c1, c2) => (L'.CApp (explifyCon c1, explifyCon c2), loc)
| L.CAbs (x, k, c) => (L'.CAbs (x, explifyKind k, explifyCon c), loc)
- | L.CDisjoint _ => raise Fail "Explify CDisjoint"
+ | L.CDisjoint (_, _, c) => explifyCon c
| L.CName s => (L'.CName s, loc)