aboutsummaryrefslogtreecommitdiff
path: root/vernac/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/classes.ml')
-rw-r--r--vernac/classes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d5509e2697..a100352145 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -57,7 +57,7 @@ let is_local_for_hint i =
let add_instance_base inst =
let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in
- add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality
+ add_instance_hint (Hints.hint_globref inst.is_impl) [inst.is_impl] ~locality
inst.is_info
let mk_instance cl info glob impl =