diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-04-12 14:19:15 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-04-12 14:19:15 -0400 |
| commit | 2f324fc9e868e0775e1401833b74af15652c6732 (patch) | |
| tree | 09447cbf30adcc3cc79bc4ebe766f74d8a60a4a9 /src/elab_env.sml | |
| parent | 84168a777e28ab53917bc3ed448cc90e6b00a4ed (diff) | |
Classes as optional arguments to Basis.tag
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 6dae1d4b..62a310f2 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -899,19 +899,19 @@ fun sgnS_con (str, (sgns, strs, cons)) c = end) | _ => c -fun sgnS_con' (arg as (m1, ms', (sgns, strs, cons))) c = - case c of - CModProj (m1, ms, x) => - (case IM.find (strs, m1) of - NONE => c - | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x)) - | CNamed n => - (case IM.find (cons, n) of - NONE => c - | SOME nx => CModProj (m1, ms', nx)) - | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1), - (sgnS_con' arg (#1 c2), #2 c2)) - | _ => c +fun sgnS_con' (m1, ms', (sgns, strs, cons)) = + U.Con.map {kind = fn x => x, + con = fn c => + case c of + CModProj (m1, ms, x) => + (case IM.find (strs, m1) of + NONE => c + | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x)) + | CNamed n => + (case IM.find (cons, n) of + NONE => c + | SOME nx => CModProj (m1, ms', nx)) + | _ => c} fun sgnS_sgn (str, (sgns, strs, cons)) sgn = case sgn of @@ -1026,7 +1026,7 @@ fun enrichClasses env classes (m1, ms) sgn = | SOME (cn, nvs, cs, c) => let val loc = #2 c - fun globalize (c, loc) = (sgnS_con' (m1, ms, fmap) c, loc) + val globalize = sgnS_con' (m1, ms, fmap) val nc = case cn of |