Mercurial > urweb
diff src/elab_util.sml @ 345:b85e6ba56618
Merge CDisjoint and TDisjoint
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 04 Oct 2008 15:50:28 -0400 |
parents | 075b36dbb1a4 |
children | dfc8c991abd0 |
line wrap: on
line diff
--- a/src/elab_util.sml Thu Sep 18 15:01:01 2008 -0400 +++ b/src/elab_util.sml Sat Oct 04 15:50:28 2008 -0400 @@ -119,14 +119,14 @@ S.map2 (mfc (bind (ctx, Rel (x, k))) c, fn c' => (TCFun (e, x, k', c'), loc))) - | TDisjoint (ai, c1, c2, c3) => + | CDisjoint (ai, c1, c2, c3) => S.bind2 (mfc ctx c1, fn c1' => S.bind2 (mfc ctx c2, fn c2' => S.map2 (mfc ctx c3, fn c3' => - (TDisjoint (ai, c1', c2', c3'), loc)))) + (CDisjoint (ai, c1', c2', c3'), loc)))) | TRecord c => S.map2 (mfc ctx c, fn c' => @@ -147,14 +147,6 @@ S.map2 (mfc (bind (ctx, Rel (x, k))) c, fn c' => (CAbs (x, k', c'), loc))) - | CDisjoint (c1, c2, c3) => - S.bind2 (mfc ctx c1, - fn c1' => - S.bind2 (mfc ctx c2, - fn c2' => - S.map2 (mfc ctx c3, - fn c3' => - (CDisjoint (c1', c2', c3'), loc)))) | CName _ => S.return2 cAll