Mercurial > urweb
diff src/elab_env.sml @ 721:9864b64b1700
Classes as optional arguments to Basis.tag
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 12 Apr 2009 14:19:15 -0400 |
parents | acb8537f58f0 |
children | 059074c8d2fc |
line wrap: on
line diff
--- a/src/elab_env.sml Sun Apr 12 12:31:54 2009 -0400 +++ b/src/elab_env.sml Sun Apr 12 14:19:15 2009 -0400 @@ -899,19 +899,19 @@ 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 @@ | 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