aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--checker/inductive.ml7
-rw-r--r--kernel/inductive.ml24
2 files changed, 16 insertions, 15 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml
index ad7c472d9..be0f220b2 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -281,9 +281,10 @@ let is_correct_arity env c (p,pj) ind specif params =
(try conv env a1 a1'
with NotConvertible -> raise (LocalArity None));
srec (push_rel (na1,None,a1) env) t ar'
- | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
- let ksort = match (whd_betadeltaiota env a2) with
- | Sort s -> family_of_sort s
+ | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
+ let env' = push_rel (na1,None,a1) env in
+ let ksort = match (whd_betadeltaiota env' a2) with
+ | Sort s -> family_of_sort s
| _ -> raise (LocalArity None) in
let dep_ind = build_dependent_inductive ind specif params in
(try conv env a1 dep_ind
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index fca72e3ae..5c1006438 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -304,18 +304,18 @@ let is_correct_arity env c pj ind specif params =
try conv env a1 a1'
with NotConvertible -> raise (LocalArity None) in
srec (push_rel (na1,None,a1) env) t ar' (union_constraints u univ)
- | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
- let ksort = match kind_of_term (whd_betadeltaiota env a2) with
- | Sort s -> family_of_sort s
- | _ -> raise (LocalArity None) in
- let dep_ind = build_dependent_inductive ind specif params in
- let univ =
- try conv env a1 dep_ind
- with NotConvertible -> raise (LocalArity None) in
- check_allowed_sort ksort specif;
- union_constraints u univ
- | _, (_,Some _,_ as d)::ar' ->
- srec (push_rel d env) (lift 1 pt') ar' u
+ (* The last Prod domain is the type of the scrutinee *)
+ | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
+ let env' = push_rel (na1,None,a1) env in
+ let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
+ | Sort s -> family_of_sort s
+ | _ -> raise (LocalArity None) in
+ let dep_ind = build_dependent_inductive ind specif params in
+ let univ =
+ try conv env a1 dep_ind
+ with NotConvertible -> raise (LocalArity None) in
+ check_allowed_sort ksort specif;
+ union_constraints u univ
| _ ->
raise (LocalArity None)
in