Module 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 -> Evd.evar_map -> Evar.t -> bool

mem allowed sigma evk is true iff evk can be defined

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

from_pred p means evars satisfying p can be defined

val except : Evar.Set.t -> t

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

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

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