Constructor

Ltac2.Constructor

type t = constructor

val equal : t -> t -> bool

equal c1 c2 tests equality of constructors. Constructors obtained through module aliases or Include are not considered equal by this function.

val inductive : t -> inductive

inductive constructor returns the inductive to which constructor belongs.

val index : t -> int

index constructor returns the index of the given constructor (such that c is Ind.get_constructor (Ind.data (inductive c)) (index c)).

val print : t -> message

print constructor prints the constructor using the shortest qualified identifier which refers to it. Does not avoid variable names in the current or global environment.