diff options
| author | coqbot-app[bot] | 2020-09-02 08:12:03 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-02 08:12:03 +0000 |
| commit | cc51e1fd680c1f1bf47cc8b504196c9f2677fa3b (patch) | |
| tree | 37c69be12d25afa112249c187bae059d949f8388 | |
| parent | 8666b46353c1f2c751bb5b6d4e1012783d107ae4 (diff) | |
| parent | c3d8ab86e892ec85acc843be62f3de9060368b13 (diff) | |
Merge PR #12883: Use a faster algorithm to check for class existence.
Reviewed-by: mattam82
| -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 |