Module Record

val primitive_flag : bool Stdlib.ref
type projection_flags = {
pf_subclass : bool;
pf_canonical : bool;
}
val declare_projections : Names.inductive -> Entries.universes_entry -> ?⁠kind:Decls.definition_object_kind -> Names.Id.t -> projection_flags list -> Impargs.manual_implicits list -> Constr.rel_context -> Recordops.proj_kind list * Names.Constant.t option list
val declare_structure_entry : Recordops.struc_tuple -> unit
val definition_structure : Constrexpr.universe_decl_expr option -> Vernacexpr.inductive_kind -> template:bool option -> cumulative:bool -> poly:bool -> Declarations.recursivity_kind -> (Vernacexpr.coercion_flag * Names.lident * Constrexpr.local_binder_expr list * (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr) list * Names.Id.t * Constrexpr.constr_expr option) list -> Names.GlobRef.t list
val declare_existing_class : Names.GlobRef.t -> unit