let itl_len = List.length itl in
let (name,_,ty,cl) = List.nth itl i in
let cl_len = List.length cl in
- if (itl_len = 1 && cl_len <= 1) then
+ if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then
let non_informative,ugraph =
if cl_len = 0 then true,ugraph
else
definition? *)
non_informative, ugraph
else
- let is_empty =
- List.fold_left
- (fun b (_,_,_,cl) -> b && List.length cl = 0) true itl
- in
- (* is it a block of mutual inductive empty definitions? *)
- is_empty,ugraph
+ false,ugraph
| _ ->
raise (TypeCheckerFailure
(lazy ("Unknown mutual inductive definition:" ^