Module Record
val primitive_flag : bool Stdlib.refval declare_projections : Names.inductive -> Entries.universes_entry -> ?kind:Decl_kinds.definition_object_kind -> Names.Id.t -> bool list -> Impargs.manual_implicits list -> Constr.rel_context -> (Names.Name.t * bool) list * Names.Constant.t option listval definition_structure : Constrexpr.universe_decl_expr option -> Vernacexpr.inductive_kind -> template:bool option -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> Declarations.recursivity_kind -> (Vernacexpr.coercion_flag * Names.lident * Constrexpr.local_binder_expr list * Vernacexpr.local_decl_expr Vernacexpr.with_instance Vernacexpr.with_priority Vernacexpr.with_notation list * Names.Id.t * Constrexpr.constr_expr option) list -> Names.GlobRef.t listval declare_existing_class : Names.GlobRef.t -> unit