From 006c487f8af220cf8a374bc38d06c3d58fe4335b Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Mon, 15 Sep 2014 14:28:35 +0200 Subject: Fix a bug in the naming of binders. The ident closure was not propagated when pretying a [uconstr] coming from a [uconstr] closure. This bug had never been reported, as far as I'm aware. --- pretyping/pretyping.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ad6a79863..d348b5eeb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -286,7 +286,11 @@ let pretype_id pretype loc env evdref lvar id = { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> try let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in - let lvar = { lvar with ltac_constrs = closure.typed; ltac_uconstrs = closure.untyped } in + let lvar = { lvar with + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents } + in (* spiwack: I'm catching [Not_found] potentially too eagerly here, as the call to the main pretyping function is caught inside the try but I want to avoid refactoring this function -- cgit v1.2.3