Module EConstr.ERelevance

Type of relevance marks up-to quality variable unification.

val make : Sorts.relevance -> t
val kind : Evd.evar_map -> t -> Sorts.relevance
val equal : Evd.evar_map -> t -> t -> bool
val relevant : t
val irrelevant : t
val is_irrelevant : Evd.evar_map -> t -> bool