diff options
| author | Pierre-Marie Pédrot | 2019-05-28 13:54:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-28 13:54:26 +0200 |
| commit | d4ca25df0f481345c99744acda28728c9682f0ac (patch) | |
| tree | cb9c1d93a219f7d4491fd52bca61478bf5f4f531 /pretyping/typing.ml | |
| parent | e005f390312b8900df36aa27bc087e18701c8fcd (diff) | |
| parent | 645ffc989659f2abaf1cb4949ac2ad4d748d6083 (diff) | |
Merge PR #10133: mind_kelim is the highest allowed sort instead of a list
Ack-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index be71f44a5e..00c52e7665 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -117,12 +117,12 @@ let check_branch_types env sigma (ind,u) cj (lfj,explft) = sigma lfj explft let max_sort l = - if Sorts.List.mem InType l then InType else - if Sorts.List.mem InSet l then InSet else InProp + if List.mem_f Sorts.family_equal InType l then InType else + if List.mem_f Sorts.family_equal InSet l then InSet else InProp let is_correct_arity env sigma c pj ind specif params = let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in - let allowed_sorts = elim_sorts specif in + let allowed_sorts = sorts_below (elim_sort specif) in let error () = Pretype_errors.error_elim_arity env sigma ind c pj None in let rec srec env sigma pt ar = let pt' = whd_all env sigma pt in @@ -135,7 +135,7 @@ let is_correct_arity env sigma c pj ind specif params = end | Sort s, [] -> let s = ESorts.kind sigma s in - if not (Sorts.List.mem (Sorts.family s) allowed_sorts) + if not (List.mem_f Sorts.family_equal (Sorts.family s) allowed_sorts) then error () else sigma, s | Evar (ev,_), [] -> @@ -199,13 +199,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let specif = lookup_mind_specif env (fst ind) in - let sorts = elim_sorts specif in + let sorts = elim_sort specif in let pj = Retyping.get_judgment_of env sigma p in let _, s = splay_prod env sigma pj.uj_type in let ksort = match EConstr.kind sigma s with | Sort s -> Sorts.family (ESorts.kind sigma s) | _ -> error_elim_arity env sigma ind c pj None in - if not (List.exists ((==) ksort) sorts) then + if not (Sorts.family_leq ksort sorts) then let s = inductive_sort_family (snd specif) in error_elim_arity env sigma ind c pj (Some(sorts,ksort,s,Type_errors.error_elim_explain ksort s)) |