Mercurial > urweb

comparison src/elab_env.sml @ 514:0fc08d1750e1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove unnecessary lifts in ElabEnv.pushCRel
author Adam Chlipala <adamc@hcoop.net>
date Thu, 27 Nov 2008 10:40:29 -0500
parents 20fab0e96217
children aceb2d982f8f
comparison
equal deleted inserted replaced
513:5fc269f744ee 514:0fc08d1750e1
266 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) 266 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
267 | x => x) (#renameC env) 267 | x => x) (#renameC env)
268 in 268 in
269 {renameC = SM.insert (renameC, x, Rel' (0, k)), 269 {renameC = SM.insert (renameC, x, Rel' (0, k)),
270 relC = (x, k) :: #relC env, 270 relC = (x, k) :: #relC env,
271 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), 271 namedC = #namedC env,
272 272
273 datatypes = #datatypes env, 273 datatypes = #datatypes env,
274 constructors = #constructors env, 274 constructors = #constructors env,
275 275
276 classes = CM.map (fn class => { 276 classes = CM.map (fn class => {
281 (#classes env), 281 (#classes env),
282 282
283 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c) 283 renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
284 | Named' (n, c) => Named' (n, lift c)) (#renameE env), 284 | Named' (n, c) => Named' (n, lift c)) (#renameE env),
285 relE = map (fn (x, c) => (x, lift c)) (#relE env), 285 relE = map (fn (x, c) => (x, lift c)) (#relE env),
286 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), 286 namedE = #namedE env,
287 287
288 renameSgn = #renameSgn env, 288 renameSgn = #renameSgn env,
289 sgn = #sgn env, 289 sgn = #sgn env,
290 290
291 renameStr = #renameStr env, 291 renameStr = #renameStr env,