diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b1c98da2c7..36b405e981 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -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 |