aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r--pretyping/typeclasses.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8d987d0379..94ade8c3c9 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -55,8 +55,9 @@ type typeclass = {
(* The method implementaions as projections. *)
cl_projs : (identifier * constant option) list;
}
+module Gmap = Fmap.Make(RefOrdered)
-type typeclasses = (global_reference, typeclass) Gmap.t
+type typeclasses = typeclass Gmap.t
type instance = {
is_class: global_reference;
@@ -68,7 +69,7 @@ type instance = {
is_impl: global_reference;
}
-type instances = (global_reference, (global_reference, instance) Gmap.t) Gmap.t
+type instances = (instance Gmap.t) Gmap.t
let instance_impl is = is.is_impl