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 /pretyping/typing.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 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b40605f228..85abe2569b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -68,6 +68,16 @@ let e_judge_of_case env evdref ci pj cj lfj = { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } +let check_allowed_sort env sigma ind c p = + let pj = Retyping.get_judgment_of env sigma p in + let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in + let specif = Global.lookup_inductive ind in + let sorts = elim_sorts specif in + if not (List.exists ((=) ksort) sorts) then + let s = inductive_sort_family (snd specif) in + error_elim_arity env ind sorts c pj + (Some(ksort,s,error_elim_explain ksort s)) + let e_judge_of_cast env evdref cj k tj = let expected_type = tj.utj_val in if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then @@ -218,4 +228,3 @@ let solve_evars env evd c = let c = (execute env evdref c).uj_val in (* side-effect on evdref *) nf_evar !evdref c - |