diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 13 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 1 |
2 files changed, 10 insertions, 4 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index e75be25f30..530fec6d10 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -111,13 +111,13 @@ let gmap_cmap_merge old ne = Gmap.fold (fun cl insts acc -> let oldinsts = try Gmap.find cl old with Not_found -> Cmap.empty in Gmap.add cl (cmap_union oldinsts insts) acc) - Gmap.empty ne + ne Gmap.empty in Gmap.fold (fun cl insts acc -> if Gmap.mem cl ne' then acc else Gmap.add cl insts acc) - ne' old - + old ne' + let add_instance_hint_ref = ref (fun id pri -> assert false) let register_add_instance_hint = (:=) add_instance_hint_ref @@ -284,9 +284,14 @@ let add_instance i = add_instance_hint i.is_impl i.is_pri; update () +let all_instances () = + Gmap.fold (fun k v acc -> + Cmap.fold (fun k v acc -> v :: acc) v acc) + !instances [] + let instances r = let cl = class_info r in instances_of cl - + let method_typeclass ref = match ref with | ConstRef c -> diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 09f6a76968..f77be52932 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -45,6 +45,7 @@ type instance val instances : global_reference -> instance list val typeclasses : unit -> typeclass list +val all_instances : unit -> instance list val add_class : typeclass -> unit |