diff options
| -rw-r--r-- | pretyping/pretyping.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 07cc36815b..3957a40a68 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -304,10 +304,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 + let lvar = { ltac_constrs = closure.typed; ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents } + ltac_idents = closure.idents; + ltac_genargs = Id.Map.empty; } in (* spiwack: I'm catching [Not_found] potentially too eagerly here, as the call to the main pretyping function is caught |