aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/classes.ml')
-rw-r--r--vernac/classes.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d99d45313..40001c0a3 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -41,7 +41,7 @@ let _ = Goptions.declare_bool_option {
let typeclasses_db = "typeclass_instances"
let set_typeclass_transparency c local b =
- Hints.add_hints local [typeclasses_db]
+ Hints.add_hints ~local [typeclasses_db]
(Hints.HintsTransparencyEntry ([c], b))
let _ =
@@ -56,7 +56,7 @@ let _ =
(Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
info.hint_pattern } in
Flags.silently (fun () ->
- Hints.add_hints local [typeclasses_db]
+ Hints.add_hints ~local [typeclasses_db]
(Hints.HintsResolveEntry
[info, poly, false, Hints.PathHints path, inst'])) ());
Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;