diff options
| author | Pierre-Marie Pédrot | 2020-08-24 15:47:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-31 10:24:43 +0200 |
| commit | c3d8ab86e892ec85acc843be62f3de9060368b13 (patch) | |
| tree | 204859d49ef1c6dea0b2db4de26a708b50278ca6 /pretyping | |
| parent | 9c9bf136430213eacec8e32ad4909cf501141a48 (diff) | |
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.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |