aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-09-01 16:14:03 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-07-03 13:39:18 +0200
commitcea3d7c83bf3aae18262e62b897ec204c098e444 (patch)
tree9ff31a628af00e19de1b8403ef94969a675e4e9d /pretyping
parentd0b1ac17610bec74abaf122628b74c62643655d8 (diff)
Remove unused env argument to fresh_sort_in_family
(Universes and Evd)
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/indrec.ml9
-rw-r--r--pretyping/typing.ml2
2 files changed, 5 insertions, 6 deletions
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' ->