aboutsummaryrefslogtreecommitdiff
path: root/pretyping/classops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.ml')
-rw-r--r--pretyping/classops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 90ce1cc594..70a9784238 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -441,7 +441,7 @@ let coercion_of_reference r =
module CoercionPrinting =
struct
type t = coe_typ
- let compare = GlobRef.Ordered.compare
+ module Set = GlobRef.Set
let encode _env = coercion_of_reference
let subst = subst_coe_typ
let printer x = Nametab.pr_global_env Id.Set.empty x