From b7fcbb07f8b484707a86eb06df1bd7116fb55a21 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 5 Oct 2011 14:34:17 +0000 Subject: 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 --- kernel/type_errors.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'kernel/type_errors.ml') diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 0f849e11a..8f129999b 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 -- cgit v1.2.3