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