diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/evar_tactics.ml | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 478019b41e..ace595a7bd 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -47,6 +47,7 @@ let instantiate_tac n (ist,rawc) ido = let lvar = { Pretyping.ltac_constrs = constrvars; ltac_uconstrs = Names.Id.Map.empty; + ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; } in let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5b0002d7e5..7d606402b0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -492,6 +492,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let vars = { Pretyping.ltac_constrs = constrvars; Pretyping.ltac_uconstrs = Id.Map.empty; + Pretyping.ltac_idents = Id.Map.empty; Pretyping.ltac_genargs = ist.lfun; } in let c = match ce with @@ -1313,6 +1314,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = let vars = { Pretyping.ltac_constrs = closure.typed; Pretyping.ltac_uconstrs = closure.untyped; + Pretyping.ltac_idents = Id.Map.empty; Pretyping.ltac_genargs = ist.lfun; } in let (sigma,c_interp) = |