summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-27 11:06:10 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-27 11:06:10 -0500
commit7fea9aa0b17626a87d36230dee7c815dcc09abbd (patch)
tree887e146d2f7fd872a74fd3591a2a68f177629b3b
parent1ca0fc2925ff1e6a195480b7687da0132b35316a (diff)
Catch another unneeded lift in ElabEnv.pushCRel
-rw-r--r--src/elab_env.sml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 3acb855d..d1084d0c 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -281,7 +281,7 @@ fun pushCRel (env : env) x k =
(#classes env),
renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c)
- | Named' (n, c) => Named' (n, lift c)) (#renameE env),
+ | Named' (n, c) => Named' (n, c)) (#renameE env),
relE = map (fn (x, c) => (x, lift c)) (#relE env),
namedE = #namedE env,