From cea3d7c83bf3aae18262e62b897ec204c098e444 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 1 Sep 2017 16:14:03 +0200 Subject: Remove unused env argument to fresh_sort_in_family (Universes and Evd) --- engine/evd.ml | 4 ++-- engine/evd.mli | 2 +- engine/univGen.ml | 4 ++-- engine/univGen.mli | 2 +- engine/universes.mli | 2 +- plugins/funind/functional_principles_types.ml | 11 +++++------ pretyping/indrec.ml | 9 ++++----- pretyping/typing.ml | 2 +- tactics/elimschemes.ml | 2 +- tactics/eqschemes.ml | 6 +++--- tactics/inv.ml | 2 +- tactics/leminv.ml | 2 +- 12 files changed, 23 insertions(+), 25 deletions(-) diff --git a/engine/evd.ml b/engine/evd.ml index 761ae7983..b39069174 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -805,8 +805,8 @@ let make_flexible_variable evd ~algebraic u = (* Operations on constants *) (****************************************) -let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = - with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family env s) +let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s = + with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s) let fresh_constant_instance ?loc env evd c = with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) diff --git a/engine/evd.mli b/engine/evd.mli index d638bb2d3..532017b36 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -598,7 +598,7 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor diff --git a/engine/univGen.ml b/engine/univGen.ml index 796a1bcc1..b07d4848f 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -215,7 +215,7 @@ let type_of_reference env r = let type_of_global t = type_of_reference (Global.env ()) t -let fresh_sort_in_family env = function +let fresh_sort_in_family = function | InProp -> Sorts.prop, ContextSet.empty | InSet -> Sorts.set, ContextSet.empty | InType -> @@ -223,7 +223,7 @@ let fresh_sort_in_family env = function Type (Univ.Universe.make u), ContextSet.singleton u let new_sort_in_family sf = - fst (fresh_sort_in_family (Global.env ()) sf) + fst (fresh_sort_in_family sf) let extend_context (a, ctx) (ctx') = (a, ContextSet.union ctx ctx') diff --git a/engine/univGen.mli b/engine/univGen.mli index 8169dbda4..439424934 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -39,7 +39,7 @@ val fresh_instance_from_context : AUContext.t -> val fresh_instance_from : AUContext.t -> Instance.t option -> Instance.t in_universe_context_set -val fresh_sort_in_family : env -> Sorts.family -> +val fresh_sort_in_family : Sorts.family -> Sorts.t in_universe_context_set val fresh_constant_instance : env -> Constant.t -> pconstant in_universe_context_set diff --git a/engine/universes.mli b/engine/universes.mli index 29673de1e..306ba0db0 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -86,7 +86,7 @@ val fresh_instance_from : AUContext.t -> Instance.t option -> Instance.t in_universe_context_set [@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"] -val fresh_sort_in_family : env -> Sorts.family -> +val fresh_sort_in_family : Sorts.family -> Sorts.t in_universe_context_set [@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"] diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 31496513a..b2a528a1f 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -322,8 +322,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) try let f = funs.(i) in - let env = Global.env () in - let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in + let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in let new_sorts = match sorts with | None -> Array.make (Array.length funs) (type_sort) @@ -344,7 +343,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = let evd' = Evd.from_env (Global.env ()) in - let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in + let evd',s = Evd.fresh_sort_in_family evd' fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in @@ -354,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Evd.const_univ_entry ~poly evd' in let ce = Declare.definition_entry ~univs value in - ignore( + ignore( Declare.declare_constant name (DefinitionEntry ce, @@ -508,8 +507,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x - ) + Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x + ) fas in (* We create the first priciple by tactic *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 4ab932723..551cc67b6 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -86,7 +86,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = if not (Sorts.List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family env kind), pind))) + (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family kind), pind))) in let ndepar = mip.mind_nrealdecls + 1 in @@ -136,7 +136,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = mkLambda_string "f" t (add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1)) in - let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in + let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg sigma kind in let typP = make_arity env' sigma dep indf s in let typP = EConstr.Unsafe.to_constr typP in let c = @@ -455,7 +455,7 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = | ((indi,u),_,_,dep,kinds)::rest -> let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list mkRel i lnamesparrec) in let s = - Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) + Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg) evdref kinds in let typP = make_arity env !evdref dep indf s in @@ -550,8 +550,7 @@ let check_arities env listdepkind = let kelim = elim_sorts (mibi,mipi) in if not (Sorts.List.mem kind kelim) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family env - kind),(mind,u)))) + (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family kind),(mind,u)))) else if Int.List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) else ni::ln) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index a66ecaaac..ca2702d74 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -138,7 +138,7 @@ let is_correct_arity env sigma c pj ind specif params = then error () else sigma | Evar (ev,_), [] -> - let sigma, s = Evd.fresh_sort_in_family env sigma (max_sort allowed_sorts) in + let sigma, s = Evd.fresh_sort_in_family sigma (max_sort allowed_sorts) in let sigma = Evd.define ev (mkSort s) sigma in sigma | _, (LocalDef _ as d)::ar' -> diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 70f73df5c..3b69d9922 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -44,7 +44,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = mib.mind_nparams_rec else mib.mind_nparams in - let sigma, sort = Evd.fresh_sort_in_family env sigma sort in + let sigma, sort = Evd.fresh_sort_in_family sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in let sigma = Evd.minimize_universes sigma in (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index ad5239116..ea5ff4a6c 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -397,7 +397,7 @@ let build_l2r_rew_scheme dep env ind kind = rel_vect (nrealargs+4) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]]) in - let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -500,7 +500,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in let realsign_ind_P n aP = name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in - let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -578,7 +578,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let realsign_ind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in - let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in diff --git a/tactics/inv.ml b/tactics/inv.ml index e467eacd9..43786c8e1 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -94,7 +94,7 @@ let make_inv_predicate env evd indf realargs id status concl = | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) | None -> let sort = get_sort_family_of env !evd concl in - let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in + let sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd sort in let p = make_arity env !evd true indf sort in let evd',(p,ptyp) = Unification.abstract_list_all env !evd p concl (realargs@[mkVar id]) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 10937322e..caf4c1eca 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -251,7 +251,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in let sigma, c = Constrintern.interp_type_evars env sigma com in - let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in + let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in try add_inversion_lemma ~poly na env sigma c sort bool tac with -- cgit v1.2.3