summaryrefslogtreecommitdiff
path: root/pretyping/detyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/detyping.ml')
-rw-r--r--pretyping/detyping.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c194a0f2..aae003b8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -532,7 +532,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
buildrec [] [] avoid env construct_nargs branch
and detype_binder isgoal bk avoid env na ty c =
- let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in
+ let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
let na',avoid' =
if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
else compute_displayed_name_in flag avoid na c in
@@ -552,9 +552,11 @@ let rec detype_rel_context where avoid env sign =
| None -> na,avoid
| Some c ->
if b<>None then
- compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c
+ compute_displayed_let_name_in
+ (RenamingElsewhereFor (env,c)) avoid na c
else
- compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in
+ compute_displayed_name_in
+ (RenamingElsewhereFor (env,c)) avoid na c in
let b = Option.map (detype false avoid env) b in
let t = detype false avoid env t in
(na',Explicit,b,t) :: aux avoid' (add_name na' env) rest