diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 00:15:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-27 15:18:11 +0200 |
| commit | b34acd7904dac581b57f7282192a40f1afb870dc (patch) | |
| tree | bf55c06c3571047063abb652b9badd6e1a463cf3 /vernac/classes.ml | |
| parent | 311e87f261b5e7f1dca61ac19d9b7b695b411ce0 (diff) | |
[tactics] Turn boolean locality hint parameter into a named one.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 61ce5d6c4..6743fe79a 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; |