Module EConstr.EInstance

type t = Evd.einstance

Type of universe instances up-to universe unification. Similar to ESorts.t for UVars.Instance.t.

val make : UVars.Instance.t -> t
val equal : Evd.evar_map -> t -> t -> bool
val empty : t
val is_empty : t -> bool
val length : t -> int * int