Constant

Ltac2.Constant

type t = constant

val equal : t -> t -> bool

equal c1 c2 tests equality of constants c1 and c2.

Constants obtained through module aliases or Include are not considered equal by this function.

val print : t -> message

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