Relevance#

Ltac2.Constr.Relevance

Type of proof relevance: relevant, irrelevant or a variable (either locally rigid variable from sort polymorphism, or unification variable from elaboration).

val equal : Evd.evar_map -> t -> t -> bool

equal sigma r1 r2 tests equality of relevances in the given evar map (the evar map matters for unification sort variables, which may be instantiated).

val relevant : t

Relevant relevance.

val irrelevant : t

Irrelevant relevance.