From fea073c74f98f3fe6728363c0f8142520ac1e50c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Sep 2020 14:42:01 +0200
Subject: Replace `frozen` by `allowed` evars in evarconv, and delay them

This is a follow-up of #9062, which introduced a discrenpancy between
the two unification engines.
---
 pretyping/evarsolve.mli | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'pretyping/evarsolve.mli')

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 3fb80432ad..89e162937d 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -16,6 +16,10 @@ type alias
 
 val of_alias : alias -> EConstr.t
 
+type allowed_evars =
+| AllowAll
+| AllowFun of (Evar.t -> bool)
+
 type unify_flags = {
   modulo_betaiota : bool;
   (* Enable beta-iota reductions during unification *)
@@ -26,8 +30,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 : allowed_evars;
+  (* 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 +45,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
-- 
cgit v1.2.3


From cd37a10f9cf5746edf16611d7f833e0e8cf2c5f8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Sep 2020 18:10:37 +0200
Subject: Abstract type for allowed evars

---
 pretyping/evarsolve.mli | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'pretyping/evarsolve.mli')

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
-- 
cgit v1.2.3


From 2724016216c88e863cd3275b406b8ec2602dfaba Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 3 Sep 2020 09:17:25 +0200
Subject: Comment AllowedEvars API

---
 pretyping/evarsolve.mli | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'pretyping/evarsolve.mli')

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
 
-- 
cgit v1.2.3