comparison src/elab_env.sml @ 517:aceb2d982f8f

Catch another unneeded lift in ElabEnv.pushCRel
author Adam Chlipala <adamc@hcoop.net>
date Thu, 27 Nov 2008 11:06:10 -0500
parents 0fc08d1750e1
children 44958d74c43f
comparison
equal deleted inserted replaced
516:11fc77fb8257 517:aceb2d982f8f
279 KM.empty (#ground class) 279 KM.empty (#ground class)
280 }) 280 })
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, 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 = #namedE env, 286 namedE = #namedE env,
287 287
288 renameSgn = #renameSgn env, 288 renameSgn = #renameSgn env,
289 sgn = #sgn env, 289 sgn = #sgn env,