+let obj_of_inductive status ~metasenv uri ind leftno il =
+ let tyl =
+ HExtlib.filter_map
+ (fun _,name,arity,cl ->
+ match classify_not_term status true [] arity with
+ | `Proposition
+ | `KindOrType
+ | `Type -> assert false (* IMPOSSIBLE *)
+ | `PropKind -> None
+ | `Kind ->
+ let arity = kind_of status ~metasenv [] arity in
+ let ctx,_ as res = split_kind_prods [] arity in
+ Some (name,ctx,[])
+ ) il
+ in
+ match tyl with
+ [] -> status,None
+ | _ -> status, Some (uri, Algebraic tyl)
+;;
+