summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-09-11 19:59:31 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-09-11 19:59:31 -0400
commita12b7d5677662153dd69c14945c0d88f447425a3 (patch)
tree6a16a83ce73b7c035f67e6d51c982e3bf79115ad /src/elab_env.sml
parenta1c9eb584060bb6fac219f53540324777a7fa5b4 (diff)
Fixed a mind-numbing De Bruijn bug
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 1b9de129..6c3d7802 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -241,7 +241,8 @@ fun pushCRel (env : env) x k =
})
(#classes env),
- renameE = #renameE env,
+ 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),