Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

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