diff options
| -rw-r--r-- | checker/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index be0f220b28..c00a6c5dd0 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -294,6 +294,8 @@ let is_correct_arity env c (p,pj) ind specif params = | Sort s', [] -> check_allowed_sort (family_of_sort s') specif; false + | _, (_,Some _,_ as d)::ar' -> + srec (push_rel d env) (lift 1 pt') ar' u | _ -> raise (LocalArity None) in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 5c10064385..abc6ba4dfb 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -316,6 +316,8 @@ let is_correct_arity env c pj ind specif params = 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 | _ -> raise (LocalArity None) in |