More efficient data structure for allowed evars

2 files changed, 8 insertions, 11 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 09e49f3253..4d5715a391 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -29,27 +29,24 @@ module AllowedEvars = struct
 
   type t =
   | AllowAll
-  | AllowFun of (Evar.t -> bool)
+  | AllowFun of (Evar.t -> bool) * Evar.Set.t
 
   let mem allowed evk =
     match allowed with
     | AllowAll -> true
-    | AllowFun f -> f evk
+    | AllowFun (f,except) -> f evk && not (Evar.Set.mem evk except)
 
-  let remove evk allowed =
-    let allowed = match allowed with
-      | AllowAll -> fun evk' -> not (Evar.equal evk evk')
-      | AllowFun f -> fun evk' -> not (Evar.equal evk evk') && f evk'
-    in
-    AllowFun allowed
+  let remove evk = function
+    | AllowAll -> AllowFun ((fun _ -> true), Evar.Set.singleton evk)
+    | AllowFun (f,except) -> AllowFun (f, Evar.Set.add evk except)
 
   let all = AllowAll
 
   let except evars =
-    AllowFun (fun evk -> not (Evar.Set.mem evk evars))
+    AllowFun ((fun _ -> true), evars)
 
   let from_pred f =
-    AllowFun f
+    AllowFun (f, Evar.Set.empty)
 
 end
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 746a237b24..207a03d80f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -417,7 +417,7 @@ let default_no_delta_unify_flags ts =
 
 let allow_new_evars sigma =
   let undefined = Evd.undefined_map sigma in
-  AllowedEvars.except @@ Evar.Map.domain undefined
+  AllowedEvars.from_pred (fun evk -> not (Evar.Map.mem evk undefined))
 
 (* Default flags for looking for subterms in elimination tactics *)
 (* Not used in practice at the current date, to the exception of *)