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/inductive.ml | |
| 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/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 8 |
1 files changed, 1 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 |