[tactics] Turn boolean locality hint parameter into a named one.

7 files changed, 8 insertions, 8 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 797dfbe23..757451882 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -320,7 +320,7 @@ let project_hint ~poly pri l2r r =
 
 let add_hints_iff ~atts l2r lc n bl =
   let open Vernacinterp in
-  Hints.add_hints (Locality.make_module_locality atts.locality) bl
+  Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl
     (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
 
 VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 643f7e99f..07047d016 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -219,7 +219,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF
     fun ~atts ~st -> begin
         let open Vernacinterp in
         let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
-        Hints.add_hints (Locality.make_section_locality atts.locality)
+        Hints.add_hints ~local:(Locality.make_section_locality atts.locality)
           (match dbnames with None -> ["core"] | Some l -> l) entry;
         st
       end
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3ade5314b..17e9775b0 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1322,7 +1322,7 @@ let interp_hints poly =
       let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
 
-let add_hints local dbnames0 h =
+let add_hints ~local dbnames0 h =
   if String.List.mem "nocore" dbnames0 then
     user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
   let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index c7de10a2a..7ec70e72e 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -178,7 +178,7 @@ val current_pure_db : unit -> hint_db list
 
 val interp_hints : polymorphic -> hints_expr -> hints_entry
 
-val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
+val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
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;
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 3bf0ca0a8..1b864b366 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -612,7 +612,7 @@ let shrink_body c ty =
 let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 
 let add_hint local prg cst =
-  Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+  Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
 
 let it_mkLambda_or_LetIn_or_clean t ctx =
   let open Context.Rel.Declaration in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e1ce4e194..7ca51db78 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -977,7 +977,7 @@ let vernac_remove_hints ~atts dbs ids =
 
 let vernac_hints ~atts lb h =
   let local = enforce_module_locality atts.locality in
-  Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h)
+  Hints.add_hints ~local lb (Hints.interp_hints atts.polymorphic h)
 
 let vernac_syntactic_definition ~atts lid x y =
   Dumpglob.dump_definition lid false "syndef";