Merge PR #12968: Replace `frozen` by `allowed` evars in evarconv, and delay them

Reviewed-by: ppedrot

1 files changed, 26 insertions, 2 deletions

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 3fb80432ad..8ff2d7fc63 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -16,6 +16,28 @@ type alias
 
 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
+  (** [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
+
 type unify_flags = {
   modulo_betaiota : bool;
   (* Enable beta-iota reductions during unification *)
@@ -26,8 +48,8 @@ type unify_flags = {
   subterm_ts : TransparentState.t;
   (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order
      unifications. *)
-  frozen_evars : Evar.Set.t;
-  (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *)
+  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
      an abstraction for an unused argument *)
@@ -41,6 +63,8 @@ type unification_result =
 
 val is_success : unification_result -> bool
 
+val is_evar_allowed : unify_flags -> Evar.t -> bool
+
 (** Replace the vars and rels that are aliases to other vars and rels by
    their representative that is most ancient in the context *)
 val expand_vars_in_term : env -> evar_map -> constr -> constr