EInstance (coq-core.EConstr.EInstance)

type t

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

val make : UVars.Instance.t -> t

val kind : Evd.evar_map -> t -> UVars.Instance.t

val empty : t

val is_empty : t -> bool