diff options
| author | Maxime Dénès | 2020-09-02 18:10:37 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-09-02 21:50:13 +0200 |
| commit | cd37a10f9cf5746edf16611d7f833e0e8cf2c5f8 (patch) | |
| tree | 98820e613bcde15378375cb06f9134e29f122d16 /pretyping/evarsolve.mli | |
| parent | fea073c74f98f3fe6728363c0f8142520ac1e50c (diff) | |
Abstract type for allowed evars
Diffstat (limited to 'pretyping/evarsolve.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 89e162937d..c248e50820 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -16,9 +16,17 @@ type alias val of_alias : alias -> EConstr.t -type allowed_evars = -| AllowAll -| AllowFun of (Evar.t -> bool) +module AllowedEvars : sig + + type t + + val all : t + val mem : t -> Evar.t -> bool + val remove : Evar.t -> t -> t + val except : Evar.Set.t -> t + val from_pred : (Evar.t -> bool) -> t + +end type unify_flags = { modulo_betaiota : bool; @@ -30,7 +38,7 @@ type unify_flags = { subterm_ts : TransparentState.t; (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order unifications. *) - allowed_evars : allowed_evars; + allowed_evars : AllowedEvars.t; (* Disallowed evars are treated like rigid variables during unification: they can not be instantiated. *) allow_K_at_toplevel : bool; (* During higher-order unifications, allow to produce K-redexes: i.e. to produce |