diff options
| author | herbelin | 2011-10-05 14:34:17 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-05 14:34:17 +0000 |
| commit | b7fcbb07f8b484707a86eb06df1bd7116fb55a21 (patch) | |
| tree | bf2bc42cc3cf39131f98f8fe687b3079bbba45d2 /kernel | |
| parent | d566330747374ba13d6b52424d53ab7d84cc921e (diff) | |
It happens that the type inference algorithm (pretyping) did not check
that the return predicate of the match construction is at an allowed
sort, resulting in tactics possibly manipulating ill-typed terms. This
is now fixed,
Incidentally removed in pretyping an ill-placed coercion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14508 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |