Record.Internaltype projection_flags = {pf_coercion : bool; |
pf_reversible : bool; |
pf_instance : bool; |
pf_priority : int option; |
pf_locality : Goptions.option_locality; |
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 listval declare_structure_entry : Structures.Structure.t -> unit