- C.Appl ((C.Rel m)::tl) when m = i ->
- (*CSC: riscrivere fermandosi a 0 *)
- (* let's check if the inductive type is applied at least to *)
- (* indparamsno parameters *)
- let last =
- List.fold_left
- (fun k x ->
- if k = 0 then 0
- else
- match CicReduction.whd context x with
- C.Rel m when m = n - (indparamsno - k) -> k - 1
- | _ ->
- raise (TypeCheckerFailure
- (lazy
- ("Non-positive occurence in mutual inductive definition(s) [1]" ^
- UriManager.string_of_uri uri)))
- ) indparamsno tl
- in
- if last = 0 then
- List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
- else
- raise (TypeCheckerFailure
- (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
- UriManager.string_of_uri uri)))
+ C.Appl ((C.Rel m)::tl) as reduct when m = i ->
+ check_homogeneous_call context indparamsno n uri reduct tl;
+ List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true