DeclareInd (u.3758aa3ddc38cffa23da0eeb3fa7893a.rocq-runtime.9.0.0.doc.rocq-runtime.vernac.DeclareInd)

Source

type one_inductive_impls =
  Impargs.manual_implicits * Impargs.manual_implicits list

Sourcetype default_dep_elim =

| DefaultElim
| PropButDepElim

Sourcetype indlocs = (Loc.t option * Loc.t option list) list

Inductive type and constructor locs, for .glob and src loc info

Source

val declare_mutual_inductive_with_eliminations : 
  ?primitive_expected:bool ->
  ?typing_flags:Declarations.typing_flags ->
  ?indlocs:indlocs ->
  ?default_dep_elim:default_dep_elim list ->
  Entries.mutual_inductive_entry ->
  UState.named_universes_entry ->
  one_inductive_impls list ->
  Names.MutInd.t

Sourcemodule Internal : sig ... end

Source

val declare_primitive_projection : 
  Names.Projection.Repr.t ->
  Names.Constant.t ->
  unit