From cea3d7c83bf3aae18262e62b897ec204c098e444 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Fri, 1 Sep 2017 16:14:03 +0200
Subject: Remove unused env argument to fresh_sort_in_family

(Universes and Evd)
---
 tactics/elimschemes.ml | 2 +-
 tactics/eqschemes.ml   | 6 +++---
 tactics/inv.ml         | 2 +-
 tactics/leminv.ml      | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'tactics')

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