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
commitefa3df8ba3084f1b494e2ce6ba4a355c00ee9d8c (patch)
tree887e146d2f7fd872a74fd3591a2a68f177629b3b
parentfaa82a140dbd3af5a59f489177ab6d43dca0ccf1 (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,