aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evd.ml4
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/univGen.ml4
-rw-r--r--engine/univGen.mli2
-rw-r--r--engine/universes.mli2
-rw-r--r--plugins/funind/functional_principles_types.ml11
-rw-r--r--pretyping/indrec.ml9
-rw-r--r--pretyping/typing.ml2
-rw-r--r--tactics/elimschemes.ml2
-rw-r--r--tactics/eqschemes.ml6
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/leminv.ml2
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 18:11:59 +0000