diff options
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 |