diff options
-rw-r--r-- | interp/constrintern.ml | 39 | ||||
-rw-r--r-- | interp/constrintern.mli | 10 | ||||
-rw-r--r-- | interp/genintern.ml | 1 | ||||
-rw-r--r-- | interp/genintern.mli | 1 | ||||
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 3 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 2 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
-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 | ||||
-rw-r--r-- | toplevel/search.ml | 4 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 4 |
14 files changed, 47 insertions, 56 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0a2a459d3..e9ebcf39f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1329,7 +1329,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalize sigma globalenv env allow_patvar lvar c = +let internalize globalenv env allow_patvar lvar c = let rec intern env = function | CRef ref as x -> let (c,imp,subscopes,l),_ = @@ -1534,7 +1534,6 @@ let internalize sigma globalenv env allow_patvar lvar c = let ist = { Genintern.ltacvars = lvars; ltacrecvars = Id.Map.empty; - gsigma = sigma; genv = globalenv; } in let (_, glb) = Genintern.generic_intern ist gen in @@ -1715,18 +1714,18 @@ type ltac_sign = Id.Set.t * Id.Set.t let empty_ltac_sign = (Id.Set.empty, Id.Set.empty) -let intern_gen kind sigma env +let intern_gen kind env ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign) c = let tmp_scope = scope_of_type_kind kind in - internalize sigma env {ids = extract_ids env; unb = false; + internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; impls = impls} allow_patvar (ltacvars, Id.Map.empty) c -let intern_constr sigma env c = intern_gen WithoutTypeConstraint sigma env c +let intern_constr env c = intern_gen WithoutTypeConstraint env c -let intern_type sigma env c = intern_gen IsType sigma env c +let intern_type env c = intern_gen IsType env c let intern_pattern globalenv patt = try @@ -1744,7 +1743,7 @@ let intern_pattern globalenv patt = (* All evars resolved *) let interp_gen kind sigma env ?(impls=empty_internalization_env) c = - let c = intern_gen kind ~impls sigma env c in + let c = intern_gen kind ~impls env c in understand ~expected_type:kind sigma env c let interp_constr sigma env ?(impls=empty_internalization_env) c = @@ -1759,13 +1758,13 @@ let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ = (* Not all evars expected to be resolved *) let interp_open_constr sigma env c = - understand_tcc sigma env (intern_constr sigma env c) + understand_tcc sigma env (intern_constr env c) (* Not all evars expected to be resolved and computation of implicit args *) let interp_constr_evars_gen_impls evdref env ?(impls=empty_internalization_env) expected_type c = - let c = intern_gen expected_type ~impls !evdref env c in + let c = intern_gen expected_type ~impls env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in understand_tcc_evars evdref env ~expected_type c, imps @@ -1781,7 +1780,7 @@ let interp_type_evars_impls evdref env ?(impls=empty_internalization_env) c = (* Not all evars expected to be resolved, with side-effect on evars *) let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) expected_type c = - let c = intern_gen expected_type ~impls !evdref env c in + let c = intern_gen expected_type ~impls env c in understand_tcc_evars evdref env ~expected_type c let interp_constr_evars evdref env ?(impls=empty_internalization_env) c = @@ -1795,16 +1794,16 @@ let interp_type_evars evdref env ?(impls=empty_internalization_env) c = (* Miscellaneous *) -let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = +let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let c = intern_gen (if as_type then IsType else WithoutTypeConstraint) - ~allow_patvar:true ~ltacvars sigma env c in + ~allow_patvar:true ~ltacvars env c in pattern_of_glob_constr c let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = Id.Map.map (fun typ -> (ref None, typ)) vars in - let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false; + let c = internalize (Global.env()) {ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impls} false (empty_ltac_sign, vl) a in (* Translate and check that [c] has all its free variables bound in [vars] *) @@ -1819,25 +1818,25 @@ let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a = (* Interpret binders and contexts *) let interp_binder sigma env na t = - let t = intern_gen IsType sigma env t in + let t = intern_gen IsType env t in let t' = locate_if_isevar (loc_of_glob_constr t) na t in understand ~expected_type:IsType sigma env t' let interp_binder_evars evdref env na t = - let t = intern_gen IsType !evdref env t in + let t = intern_gen IsType env t in let t' = locate_if_isevar (loc_of_glob_constr t) na t in understand_tcc_evars evdref env ~expected_type:IsType t' open Environ -let my_intern_constr sigma env lvar acc c = - internalize sigma env acc false lvar c +let my_intern_constr env lvar acc c = + internalize env acc false lvar c -let intern_context global_level sigma env impl_env binders = +let intern_context global_level env impl_env binders = try let lvar = (empty_ltac_sign, Id.Map.empty) in let lenv, bl = List.fold_left - (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) lvar) + (intern_local_binder_aux ~global_level (my_intern_constr env lvar) lvar) ({ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impl_env}, []) binders in (lenv.impls, List.map snd bl) @@ -1869,7 +1868,7 @@ let interp_rawcontext_evars evdref env bl = in (env, par), impls let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params = - let int_env,bl = intern_context global_level !evdref env impl_env params in + let int_env,bl = intern_context global_level env impl_env params in let x = interp_rawcontext_evars evdref env bl in int_env, x diff --git a/interp/constrintern.mli b/interp/constrintern.mli index a4f3e057f..bbee24957 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -74,18 +74,18 @@ type glob_binder = (Name.t * binding_kind * glob_constr option * glob_constr) (** {6 Internalization performs interpretation of global names and notations } *) -val intern_constr : evar_map -> env -> constr_expr -> glob_constr +val intern_constr : env -> constr_expr -> glob_constr -val intern_type : evar_map -> env -> constr_expr -> glob_constr +val intern_type : env -> constr_expr -> glob_constr -val intern_gen : typing_constraint -> evar_map -> env -> +val intern_gen : typing_constraint -> env -> ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> Id.t list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list +val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list (** {6 Composing internalization with type inference (pretyping) } *) @@ -132,7 +132,7 @@ val interp_type_evars_impls : evar_map ref -> env -> (** Interprets constr patterns *) val intern_constr_pattern : - evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> + env -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) diff --git a/interp/genintern.ml b/interp/genintern.ml index d1bc28333..fef32a5ff 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -15,7 +15,6 @@ open Genarg type glob_sign = { ltacvars : Id.Set.t; ltacrecvars : Nametab.ltac_constant Id.Map.t; - gsigma : Evd.evar_map; genv : Environ.env } type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb diff --git a/interp/genintern.mli b/interp/genintern.mli index 7027315e7..970f27f66 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -13,7 +13,6 @@ open Genarg type glob_sign = { ltacvars : Id.Set.t; ltacrecvars : Nametab.ltac_constant Id.Map.t; - gsigma : Evd.evar_map; genv : Environ.env } (** {5 Internalization functions} *) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b21037d25..6e53ae6a2 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1456,8 +1456,7 @@ let do_instr raw_instr pts = let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in let gl = { it=List.hd gls ; sigma=sigma; } in let env= pf_env gl in - let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - gsigma = sigma; genv = env} in + let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) sigma env glob_instr in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dc59b7ca..661e5e486 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -131,7 +131,7 @@ let rec abstract_glob_constr c = function (abstract_glob_constr c bl) let interp_casted_constr_with_implicits sigma env impls c = - Constrintern.intern_gen Pretyping.WithoutTypeConstraint sigma env ~impls + Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls ~allow_patvar:false ~ltacvars:(Id.Set.empty, Id.Set.empty) c (* diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b7c471f4a..ac54e44cc 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -71,7 +71,7 @@ let isVarf f x = let ident_global_exist id = try let ans = CRef (Libnames.Ident (Loc.ghost,id)) in - let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in + let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in true with e when Errors.noncritical e -> false diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 36ba80202..8c2776789 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -63,7 +63,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let instantiate_pf_com evk com sigma = let evi = Evd.find sigma evk in let env = Evd.evar_filtered_env evi in - let rawc = Constrintern.intern_constr sigma env com in + let rawc = Constrintern.intern_constr env com in let ltac_vars = (Id.Map.empty, Id.Map.empty) in let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in sigma' diff --git a/tactics/auto.ml b/tactics/auto.ml index 9156e1f04..fc9a335e6 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 59bad5808..7f676c157 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 c04b6f391..8473f585b 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 2e5465340..433322e4c 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) (***************************************************************************) diff --git a/toplevel/search.ml b/toplevel/search.ml index 9e61bc7fb..91762c000 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -247,11 +247,11 @@ let interface_search flags = extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l | (Interface.Type_Pattern s, b) :: l -> let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + let (_, pat) = Constrintern.intern_constr_pattern env constr in extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l | (Interface.SubType_Pattern s, b) :: l -> let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + let (_, pat) = Constrintern.intern_constr_pattern env constr in extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l | (Interface.In_Module m, b) :: l -> let path = String.concat "." m in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index db51ff610..399471b74 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1431,7 +1431,7 @@ open Search let interp_search_about_item = function | SearchSubPattern pat -> - let _,pat = intern_constr_pattern Evd.empty (Global.env()) pat in + let _,pat = intern_constr_pattern (Global.env()) pat in GlobSearchSubPattern pat | SearchString (s,None) when Id.is_valid s -> GlobSearchString s @@ -1448,7 +1448,7 @@ let interp_search_about_item = function let vernac_search s r = let r = interp_search_restriction r in let env = Global.env () in - let get_pattern c = snd (Constrintern.intern_constr_pattern Evd.empty env c) in + let get_pattern c = snd (Constrintern.intern_constr_pattern env c) in match s with | SearchPattern c -> msg_notice (Search.search_pattern (get_pattern c) r) |