Names.Construct
type t = Ind.t * int
Designation of a (particular) constructor of a (particular) inductive type.
val modpath : t -> ModPath.t
include QNameS with type t := t
module CanOrd : EqType with type t = t
Equality functions over the canonical name. Their use should be restricted to the kernel.
module UserOrd : EqType with type t = t
Equality functions over the user name.
module SyntacticOrd : EqType with type t = t
Equality functions using both names, for low-level uses.