diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-09-01 16:14:03 +0200 |
|---|---|---|
| committer |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:39:18 +0200 |
| commit | cea3d7c83bf3aae18262e62b897ec204c098e444 (patch) | |
| tree | 9ff31a628af00e19de1b8403ef94969a675e4e9d /tactics | |
| parent | d0b1ac17610bec74abaf122628b74c62643655d8 (diff) | |
Remove unused env argument to fresh_sort_in_family
(Universes and Evd)
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elimschemes.ml | 2 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 6 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 |
4 files changed, 6 insertions, 6 deletions
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 |