Internal (rocq-runtime.Record.Internal)

val declare_projections : 
  Names.inductive ->
  kind:Decls.definition_object_kind ->
  inhabitant_id:Names.Id.t ->
  Data.projection_flags list ->
  ?fieldlocs:Loc.t option list ->
  Impargs.manual_implicits list ->
  Structures.Structure.projection list

val declare_structure_entry : Structures.Structure.t -> unit