diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2018-06-14 11:48:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2018-06-14 11:48:49 +0200 |
| commit | b5569f511338ebdc7d1053b25500acbffa3e3a40 (patch) | |
| tree | 6cc5d6c970f9cd8f38152e5c4aa4e1cbd2362fbb /pretyping | |
| parent | e40e2e7bb250686836693911717d7acfee72ba81 (diff) | |
| parent | f1eac254c130af383587455876b4000fe0cdf957 (diff) | |
Merge PR #664: Fixing #5500 (missing test in return clause of match leading to anomaly)
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 1 | ||||
| -rw-r--r-- | pretyping/typing.ml | 7 |
2 files changed, 6 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aa1c23f52..6e1d3e551 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1427,6 +1427,7 @@ and match_current pb (initial,tomatch) = let case = make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in + let _ = Typing.e_type_of pb.env pb.evdref pred in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; { uj_val = applist (case, inst); uj_type = prod_applist !(pb.evdref) typ inst } diff --git a/pretyping/typing.ml b/pretyping/typing.ml index bffe36eea..cf34ac016 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -197,10 +197,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = - let pj = Retyping.get_judgment_of env sigma p in - let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in + let pj = Retyping.get_judgment_of env sigma p in + let _, s = splay_prod env sigma pj.uj_type in + let ksort = match EConstr.kind sigma s with + | Sort s -> Sorts.family (ESorts.kind sigma s) + | _ -> error_elim_arity env sigma ind sorts c pj None in if not (List.exists ((==) ksort) sorts) then let s = inductive_sort_family (snd specif) in error_elim_arity env sigma ind sorts c pj |