From c3d8ab86e892ec85acc843be62f3de9060368b13 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Aug 2020 15:47:07 +0200
Subject: Use a faster algorithm to check for class existence.

There is a hidden invariant that guarantees that the class index and its
reference field are the same.
---
 pretyping/typeclasses.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d1b65775bd..adb9c5299f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -68,6 +68,7 @@ type typeclass = {
 }
 
 type typeclasses = typeclass GlobRef.Map.t
+(* Invariant: for any pair (gr, tc) in the map, gr and tc.cl_impl are equal *)
 
 type instance = {
   is_class: GlobRef.t;
@@ -268,7 +269,7 @@ let instances env sigma r =
   let cl = class_info env sigma r in instances_of cl
 
 let is_class gr =
-  GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
+  GlobRef.Map.mem gr !classes
 
 open Evar_kinds
 type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
-- 
cgit v1.2.3