diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-15 14:28:35 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-15 15:44:10 +0200 |
| commit | 006c487f8af220cf8a374bc38d06c3d58fe4335b (patch) | |
| tree | e1f7c58a6c6ae4ef1fe9d45b207ee709747bb320 | |
| parent | 708f0634b75b784f9196d063edd19274bbb43425 (diff) | |
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.
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 |