diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index e73a78fb8..4386144fe 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -71,10 +71,10 @@ type typeclass = { cl_univs : Univ.AUContext.t; (* The class implementation *) - cl_impl : global_reference; + cl_impl : GlobRef.t; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : global_reference option list * Context.Rel.t; + cl_context : GlobRef.t option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -91,12 +91,12 @@ type typeclass = { type typeclasses = typeclass Refmap.t type instance = { - is_class: global_reference; + is_class: GlobRef.t; is_info: hint_info_expr; (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; - is_impl: global_reference; + is_impl: GlobRef.t; } type instances = (instance Refmap.t) Refmap.t @@ -480,7 +480,7 @@ let instances r = let cl = class_info r in instances_of cl let is_class gr = - Refmap.exists (fun _ v -> eq_gr v.cl_impl gr) !classes + Refmap.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes let is_instance = function | ConstRef c -> |