diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 14 | ||||
| -rw-r--r-- | tactics/tacintern.mli | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 18 |
4 files changed, 15 insertions, 20 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 9156e1f04d..fc9a335e68 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -859,7 +859,7 @@ let interp_hints = let path, gr = fi c in (o, b, path, gr) in - let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in + let fp = Constrintern.intern_constr_pattern (Global.env()) in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 59bad5808a..7f676c157a 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -57,12 +57,10 @@ type glob_sign = Genintern.glob_sign = { (* ltac variables and the subset of vars introduced by Intro/Let/... *) ltacrecvars : ltac_constant Id.Map.t; (* ltac recursive names *) - gsigma : Evd.evar_map; genv : Environ.env } let fully_empty_glob_sign = - { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - gsigma = Evd.empty; genv = Environ.empty_env } + { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = Environ.empty_env } let make_empty_glob_sign () = { fully_empty_glob_sign with genv = Global.env () } @@ -252,12 +250,12 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c = +let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = (lfun, Id.Set.empty) in let c' = - warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c + warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c in (c',if !strict_check then None else Some c) @@ -330,7 +328,7 @@ let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c) let intern_constr_pattern ist ~as_type ~ltacvars pc = let ltacvars = ltacvars, Id.Set.empty in let metas,pat = Constrintern.intern_constr_pattern - ist.gsigma ist.genv ~as_type ~ltacvars pc + ist.genv ~as_type ~ltacvars pc in let c = intern_constr_gen true false ist pc in metas,(c,pat) @@ -701,7 +699,7 @@ and intern_match_rule onlytac ist = function | (All tc)::tl -> All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl) | (Pat (rl,mp,tc))::tl -> - let {ltacvars=lfun; gsigma=sigma; genv=env} = ist in + let {ltacvars=lfun; genv=env} = ist in let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in let ido,metas2,pat = intern_pattern ist lfun mp in let fold accu x = Id.Set.add x accu in @@ -760,7 +758,7 @@ let glob_tactic_env l env x = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in Flags.with_option strict_check (intern_pure_tactic - { ltacvars; ltacrecvars = Id.Map.empty; gsigma = Evd.empty; genv = env }) + { ltacvars; ltacrecvars = Id.Map.empty; genv = env }) x let split_ltac_fun = function diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index c04b6f3912..8473f585bd 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -26,7 +26,6 @@ open Nametab type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; ltacrecvars : ltac_constant Id.Map.t; - gsigma : Evd.evar_map; genv : Environ.env } val fully_empty_glob_sign : glob_sign diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2e54653403..433322e4c1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -485,7 +485,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let ltacvars = Id.Map.domain constrvars in let bndvars = Id.Map.domain ist.lfun in let ltacdata = (ltacvars, bndvars) in - intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c + intern_gen kind ~allow_patvar ~ltacvars:ltacdata env c in let trace = push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in @@ -2078,8 +2078,7 @@ let eval_tactic_ist ist t = let interp_tac_gen lfun avoid_ids debug t = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in let ist = { lfun = lfun; extra = extra } in @@ -2087,7 +2086,7 @@ let interp_tac_gen lfun avoid_ids debug t = interp_tactic ist (intern_pure_tactic { ltacvars; ltacrecvars = Id.Map.empty; - gsigma = sigma; genv = env } t) + genv = env } t) end let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t @@ -2101,9 +2100,9 @@ let eval_ltac_constr t = (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) let hide_interp global t ot = - let hide_interp env sigma = + let hide_interp env = let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - gsigma = sigma; genv = env } in + genv = env } in let te = intern_pure_tactic ist t in let t = eval_tactic te in match ot with @@ -2112,11 +2111,10 @@ let hide_interp global t ot = in if global then Proofview.tclENV >= fun env -> - Proofview.tclEVARMAP >= fun sigma -> - hide_interp env sigma + hide_interp env else Proofview.Goal.enter begin fun gl -> - hide_interp (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) + hide_interp (Proofview.Goal.env gl) end (***************************************************************************) @@ -2170,7 +2168,7 @@ let () = let interp_redexp env sigma r = let ist = default_ist () in - let gist = { fully_empty_glob_sign with genv = env; gsigma = sigma } in + let gist = { fully_empty_glob_sign with genv = env; } in interp_red_expr ist sigma env (intern_red_expr gist r) (***************************************************************************) |