From 4e0f9f5638df5ea6061ee82e1c8314054f72c903 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Sep 2020 21:49:42 +0200
Subject: More efficient data structure for allowed evars

---
 pretyping/evarsolve.ml | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

(limited to 'pretyping/evarsolve.ml')

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