Module Names.ProjectionSource

Sourcemodule Repr : sig ... end
Sourcetype t
Sourceval make : Repr.t -> bool -> t
Sourceval repr : t -> Repr.t
include QNameS with type t := t
Sourcemodule CanOrd : EqType with type t = t

Equality functions over the canonical name. Their use should be restricted to the kernel.

Sourcemodule UserOrd : EqType with type t = t

Equality functions over the user name.

Sourcemodule SyntacticOrd : EqType with type t = t

Equality functions using both names, for low-level uses.

Sourceval canonize : t -> t

Returns the canonical version of the name

Sourceval constant : t -> Constant.t
Sourceval mind : t -> MutInd.t
Sourceval inductive : t -> inductive
Sourceval npars : t -> int
Sourceval arg : t -> int
Sourceval label : t -> Label.t
Sourceval unfolded : t -> bool
Sourceval unfold : t -> t
Sourceval equal : t -> t -> bool
  • deprecated Use QProjection.equal
Sourceval hash : t -> int
  • deprecated Use QProjection.hash
Sourceval hcons : t -> t

Hashconsing of projections.

Sourceval repr_equal : t -> t -> bool

Ignoring the unfolding boolean.

  • deprecated Use an explicit projection of Repr
Sourceval compare : t -> t -> int
  • deprecated Use QProjection.compare
Sourceval map : (MutInd.t -> MutInd.t) -> t -> t
Sourceval map_npars : (int -> int) -> t -> t
Sourceval to_string : t -> string

Encode as a string (not to be used for user-facing messages).

Sourceval print : t -> Pp.t

Print internal representation (not to be used for user-facing messages).

Sourceval debug_to_string : t -> string

Same as to_string, but outputs extra information related to debug.

Sourceval debug_print : t -> Pp.t

Same as print, but outputs extra information related to debug.