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