Module `Record.Internal`

type projection_flags = { pf_subclass : bool; pf_canonical : bool; }

val declare_projections : Names.inductive -> (Entries.universes_entry * UnivNames.universe_binders) -> ?⁠kind:Decls.definition_object_kind -> Names.Id.t -> projection_flags list -> Impargs.manual_implicits list -> Constr.rel_context -> Structures.Structure.projection list
val declare_structure_entry : Structures.Structure.t -> unit