diff src/elab_env.sml @ 514:0fc08d1750e1

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
line wrap: on
line diff
--- a/src/elab_env.sml	Thu Nov 27 10:13:22 2008 -0500
+++ b/src/elab_env.sml	Thu Nov 27 10:40:29 2008 -0500
@@ -268,7 +268,7 @@
     in
         {renameC = SM.insert (renameC, x, Rel' (0, k)),
          relC = (x, k) :: #relC env,
-         namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
+         namedC = #namedC env,
 
          datatypes = #datatypes env,
          constructors = #constructors env,
@@ -283,7 +283,7 @@
          renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
                             | Named' (n, c) => Named' (n, lift c)) (#renameE env),
          relE = map (fn (x, c) => (x, lift c)) (#relE env),
-         namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
+         namedE = #namedE env,
 
          renameSgn = #renameSgn env,
          sgn = #sgn env,