diff options
author | 2012-03-27 07:48:23 +0200 | |
---|---|---|
committer | 2012-03-27 07:48:23 +0200 | |
commit | ad988252cac876f0b9998b5223f565d0a22aebb8 (patch) | |
tree | 0c0e0cd5c943b3fbeb97c99cf46e19bbc97144c0 /pretyping/detyping.ml | |
parent | 11b04078a227fd8849972d05417487520177fb04 (diff) | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) |
Merge tag 'upstream/8.3.pl4+dfsg'
Upstream version 8.3.pl4+dfsg
Diffstat (limited to 'pretyping/detyping.ml')
-rw-r--r-- | pretyping/detyping.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 14e72807..fe4354b6 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: detyping.ml 15069 2012-03-20 14:06:07Z herbelin $ *) open Pp open Util @@ -533,7 +533,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 @@ -553,9 +553,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 |