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/inductiveops.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/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b1c98da2c7..12a7859b88 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -255,10 +255,13 @@ let inductive_has_local_defs env ind = let l2 = mib.mind_nparams + mip.mind_nrealargs in not (Int.equal l1 l2) -let allowed_sorts env (kn,i as ind) = +let top_allowed_sort env (kn,i as ind) = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_kelim +let sorts_below top = + List.filter (fun s -> Sorts.family_leq s top) Sorts.[InSProp;InProp;InSet;InType] + let has_dependent_elim mib = match mib.mind_record with | PrimRecord _ -> mib.mind_finite == BiFinite |