Remove unused env argument to fresh_sort_in_family

(Universes and Evd)

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