diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 8 | ||||
| -rw-r--r-- | kernel/type_errors.ml | 5 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 1 |
3 files changed, 7 insertions, 7 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index aeeefbfa42..21f86233ab 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -233,12 +233,6 @@ let type_of_constructors ind (mib,mip) = (************************************************************************) -let error_elim_expln kp ki = - match kp,ki with - | (InType | InSet), InProp -> NonInformativeToInformative - | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *) - | _ -> WrongArity - (* Type of case predicates *) let local_rels ctxt = @@ -290,7 +284,7 @@ exception LocalArity of (sorts_family * sorts_family * arity_error) option let check_allowed_sort ksort specif = if not (List.exists ((=) ksort) (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in - raise (LocalArity (Some(ksort,s,error_elim_expln ksort s))) + raise (LocalArity (Some(ksort,s,error_elim_explain ksort s))) let is_correct_arity env c pj ind specif params = let arsign,_ = get_instantiated_arity specif params in diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 0f849e11ab..8f129999b4 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -109,4 +109,9 @@ let error_ill_formed_rec_body env why lna i fixenv vdefj = let error_ill_typed_rec_body env i lna vdefj vargs = raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs))) +let error_elim_explain kp ki = + match kp,ki with + | (InType | InSet), InProp -> NonInformativeToInformative + | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *) + | _ -> WrongArity diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 2bf96f3227..7c61e10571 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -97,3 +97,4 @@ val error_ill_formed_rec_body : val error_ill_typed_rec_body : env -> int -> name array -> unsafe_judgment array -> types array -> 'a +val error_elim_explain : sorts_family -> sorts_family -> arity_error |