diff options
Diffstat (limited to 'checker/inductive.ml')
-rw-r--r-- | checker/inductive.ml | 7 |
1 files changed, 4 insertions, 3 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 |