diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 60bc784f1f..62f7d4d653 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -248,7 +248,6 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = let ltacvars = { Constrintern.ltac_vars = lfun; ltac_bound = Id.Set.empty; - ltac_subst = Id.Map.empty; } in let c' = warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c @@ -328,7 +327,6 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc = let ltacvars = { Constrintern.ltac_vars = ltacvars; ltac_bound = Id.Set.empty; - ltac_subst = Id.Map.empty; } in let metas,pat = Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars pc diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 9ec486c1c3..c346a7cd35 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -480,7 +480,6 @@ let interp_uconstr ist env = function let ltacvars = { Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped)); ltac_bound = Id.Map.domain ist.lfun; - ltac_subst = Id.Map.empty; } in { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } @@ -496,7 +495,6 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let ltacvars = { ltac_vars = Id.Map.domain constrvars; ltac_bound = Id.Map.domain ist.lfun; - ltac_subst = Id.Map.empty; } in intern_gen kind ~allow_patvar ~ltacvars env c in |