From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- pretyping/detyping.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'pretyping/detyping.ml') 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 -- cgit v1.2.3