diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-01-15 18:51:36 -0500 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-01-15 18:51:36 -0500 |
| commit | 082b9f2efb4a775caa2b49dafc1dfcfd09cf9948 (patch) | |
| tree | f5b50004ab480491d780510e97b0e426a0958712 | |
| parent | b2454de95c601785cb4a081fc2902cec14b9b266 (diff) | |
Christmas is over...
| -rw-r--r-- | checker/inductive.ml | 7 | ||||
| -rw-r--r-- | kernel/inductive.ml | 24 |
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 |