diff options
| -rw-r--r-- | pretyping/evarsolve.mli | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index c248e50820..8ff2d7fc63 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -19,12 +19,22 @@ val of_alias : alias -> EConstr.t module AllowedEvars : sig 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 - val remove : Evar.t -> t -> t - val except : Evar.Set.t -> t + (** [mem allowed 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] *) end |