package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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.