From cea3d7c83bf3aae18262e62b897ec204c098e444 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 1 Sep 2017 16:14:03 +0200 Subject: Remove unused env argument to fresh_sort_in_family (Universes and Evd) --- pretyping/indrec.ml | 9 ++++----- pretyping/typing.ml | 2 +- 2 files changed, 5 insertions(+), 6 deletions(-) (limited to 'pretyping') 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' -> -- cgit v1.2.3 From 26f228a4b15c270212bd2b33419400ef7d08f92a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 5 Sep 2017 15:55:30 +0200 Subject: Glob_ops.fix_kind_eq: fix typo --- pretyping/glob_ops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index ba193da60..988bdae03 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -112,7 +112,7 @@ let fix_kind_eq f k1 k2 = match k1, k2 with let eq (i1, o1) (i2, o2) = Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2 in - Int.equal i1 i2 && Array.equal eq a1 a1 + Int.equal i1 i2 && Array.equal eq a1 a2 | GCoFix i1, GCoFix i2 -> Int.equal i1 i2 | (GFix _ | GCoFix _), _ -> false -- cgit v1.2.3 From f50c823eb90af7088e2efec9e2c462dcacd12613 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 5 Sep 2017 15:57:13 +0200 Subject: Glob_ops.rename_glob_vars: fix typo --- pretyping/glob_ops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 988bdae03..4dfa789ba 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -452,7 +452,7 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function else r | GProd (na,bk,t,c) -> let na',l' = update_subst na l in - GProd (na,bk,rename_glob_vars l t,rename_glob_vars l' c) + GProd (na',bk,rename_glob_vars l t,rename_glob_vars l' c) | GLambda (na,bk,t,c) -> let na',l' = update_subst na l in GLambda (na',bk,rename_glob_vars l t,rename_glob_vars l' c) -- cgit v1.2.3