DeclareInd (p.rocq-runtime.9.2.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

Sourcetype declare_schemes =

| None
| Default

Sourceval schemes_attr : declare_schemes Attributes.attribute

Source

val declare_mutual_inductive_with_eliminations : 
  ?typing_flags:Declarations.typing_flags ->
  ?indlocs:indlocs ->
  ?default_dep_elim:default_dep_elim list ->
  ?schemes:declare_schemes ->
  ?all_depth:int ->
  Entries.mutual_inductive_entry ->
  UState.named_universes_entry ->
  one_inductive_impls list ->
  Names.MutInd.t

Source

val do_scheme_all : 
  Libnames.qualid Constrexpr.or_by_notation ->
  Names.Id.t list option ->
  unit

Create the All predicate with its theorem all_forall.

Sourcemodule Internal : sig ... end

Source

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