Names.Ind
type t = MutInd.t * int
Designation 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.
val canonize : t -> t
Returns the canonical version of the name