Evarsolve.AllowedEvars

type t

Represents the set of evars that can be defined by the pretyper

val all : t

All evars can be defined

val mem : t -> Evar.t -> bool

mem allowed evk is true iff evk can be defined

mem allowed evk

val from_pred : (Evar.t -> bool) -> t

from_pred p means evars satisfying p can be defined

from_pred p

val except : Evar.Set.t -> t

except evars means all evars can be defined except the ones in evars

except evars

evars

val remove : Evar.t -> t -> t

remove evk allowed removes evk from the set of evars allowed by allowed

remove evk allowed

evk

allowed