-type obj =
- | Constant of NUri.uri * metasenv * substitution * relevance * string * term option * term * c_attr
- | Fixpoint of NUri.uri * metasenv * substitution * bool * inductiveFun list * f_attr
- | Inductive of NUri.uri * metasenv * substitution * bool * int * inductiveType list * i_attr
- (* uri, menv, subst, (co)inductive, leftno, types *)
+type obj_kind =
+ | Constant of relevance * string * term option * term * c_attr
+ | Fixpoint of bool * inductiveFun list * f_attr
+ | Inductive of bool * int * inductiveType list * i_attr
+ (* (co)inductive, leftno, types *)