Merge PR #13388: Export locality for all hint commands

Reviewed-by: silene
Reviewed-by: gares
Reviewed-by: Zimmi48

8 files changed, 250 insertions, 58 deletions

diff --git a/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst
new file mode 100644
index 0000000000..df2bdfeabb
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  The :attr:`export` locality can now be used for all Hint commands,
+  including Hint Cut, Hint Mode, Hint Transparent / Opaque and
+  Remove Hints
+  (`#13388 <https://github.com/coq/coq/pull/13388>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index e6dc6f6c51..485b92342d 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -280,9 +280,7 @@ automatically created.
      sections.
 
    + :attr:`export` are visible from other modules when they import the current
-     module. Requiring it is not enough. This attribute is only effective for
-     the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and
-     :cmd:`Hint Extern` variants of the command.
+     module. Requiring it is not enough.
 
    + :attr:`global` hints are made available by merely requiring the current
      module.
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 44472a1995..15861d49be 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -240,10 +240,21 @@ ARGUMENT EXTEND opthints
 END
 
 VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
-| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
-        let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
-        let locality = if Locality.make_section_locality locality then Goptions.OptLocal else Goptions.OptGlobal in
-        Hints.add_hints ~locality
-          (match dbnames with None -> ["core"] | Some l -> l) entry;
+| #[ locality = Attributes.option_locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
+  let open Goptions in
+  let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
+  let () = match locality with
+  | OptGlobal ->
+    if Global.sections_are_opened () then
+    CErrors.user_err Pp.(str
+      "This command does not support the global attribute in sections.");
+  | OptExport ->
+    if Global.sections_are_opened () then
+    CErrors.user_err Pp.(str
+      "This command does not support the export attribute in sections.");
+  | OptDefault | OptLocal -> ()
+  in
+  Hints.add_hints ~locality
+    (match dbnames with None -> ["core"] | Some l -> l) entry;
  }
 END
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 68229dbe26..6fab111e6f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1023,11 +1023,15 @@ let remove_hint dbname grs =
 
 type hint_action =
   | CreateDB of bool * TransparentState.t
-  | AddTransparency of evaluable_global_reference hints_transparency_target * bool
+  | AddTransparency of {
+      superglobal : bool;
+      grefs : evaluable_global_reference hints_transparency_target;
+      state : bool;
+    }
   | AddHints of { superglobal : bool; hints : hint_entry list }
-  | RemoveHints of GlobRef.t list
-  | AddCut of hints_path
-  | AddMode of GlobRef.t * hint_mode array
+  | RemoveHints of { superglobal : bool; hints : GlobRef.t list }
+  | AddCut of { superglobal : bool; paths : hints_path }
+  | AddMode of { superglobal : bool; gref : GlobRef.t; mode : hint_mode array }
 
 let add_cut dbname path =
   let db = get_db dbname in
@@ -1049,12 +1053,16 @@ let load_autohint _ (kn, h) =
   let name = h.hint_name in
   match h.hint_action with
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b)
-  | AddTransparency (grs, b) -> add_transparency name grs b
+  | AddTransparency { superglobal; grefs; state } ->
+    if superglobal then add_transparency name grefs state
   | AddHints { superglobal; hints } ->
     if superglobal then add_hint name hints
-  | RemoveHints grs -> remove_hint name grs
-  | AddCut path -> add_cut name path
-  | AddMode (l, m) -> add_mode name l m
+  | RemoveHints { superglobal; hints } ->
+    if superglobal then remove_hint name hints
+  | AddCut { superglobal; paths } ->
+    if superglobal then add_cut name paths
+  | AddMode { superglobal; gref; mode } ->
+    if superglobal then add_mode name gref mode
 
 let open_autohint i (kn, h) =
   if Int.equal i 1 then match h.hint_action with
@@ -1067,7 +1075,15 @@ let open_autohint i (kn, h) =
     in
     let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in
     List.iter add hints
-  | _ -> ()
+  | AddCut { superglobal; paths } ->
+    if not superglobal then add_cut h.hint_name paths
+  | AddTransparency { superglobal; grefs; state } ->
+    if not superglobal then add_transparency h.hint_name grefs state
+  | RemoveHints { superglobal; hints } ->
+    if not superglobal then remove_hint h.hint_name hints
+  | AddMode { superglobal; gref; mode } ->
+    if not superglobal then add_mode h.hint_name gref mode
+  | CreateDB _ -> ()
 
 let cache_autohint (kn, obj) =
   load_autohint 1 (kn, obj); open_autohint 1 (kn, obj)
@@ -1124,7 +1140,7 @@ let subst_autohint (subst, obj) =
   in
   let action = match obj.hint_action with
     | CreateDB _ -> obj.hint_action
-    | AddTransparency (target, b) ->
+    | AddTransparency { superglobal; grefs = target; state = b } ->
       let target' =
         match target with
         | HintsVariables -> target
@@ -1134,19 +1150,19 @@ let subst_autohint (subst, obj) =
           if grs == grs' then target
           else HintsReferences grs'
       in
-      if target' == target then obj.hint_action else AddTransparency (target', b)
+      if target' == target then obj.hint_action else AddTransparency { superglobal; grefs = target'; state = b }
     | AddHints { superglobal; hints } ->
       let hints' = List.Smart.map subst_hint hints in
       if hints' == hints then obj.hint_action else AddHints { superglobal; hints = hints' }
-    | RemoveHints grs ->
+    | RemoveHints { superglobal; hints = grs } ->
       let grs' = List.Smart.map (subst_global_reference subst) grs in
-      if grs == grs' then obj.hint_action else RemoveHints grs'
-    | AddCut path ->
+      if grs == grs' then obj.hint_action else RemoveHints { superglobal; hints = grs' }
+    | AddCut { superglobal; paths = path } ->
       let path' = subst_hints_path subst path in
-      if path' == path then obj.hint_action else AddCut path'
-    | AddMode (l,m) ->
+      if path' == path then obj.hint_action else AddCut { superglobal; paths = path' }
+    | AddMode { superglobal; gref = l; mode = m } ->
       let l' = subst_global_reference subst l in
-      if l' == l then obj.hint_action else AddMode (l', m)
+      if l' == l then obj.hint_action else AddMode { superglobal; gref = l'; mode = m }
   in
   if action == obj.hint_action then obj else { obj with hint_action = action }
 
@@ -1173,11 +1189,17 @@ let create_hint_db l n st b =
   let hint = make_hint ~local:l n (CreateDB (b, st)) in
   Lib.add_anonymous_leaf (inAutoHint hint)
 
-let remove_hints local dbnames grs =
+let interp_locality = function
+| Goptions.OptDefault | Goptions.OptGlobal -> false, true
+| Goptions.OptExport -> false, false
+| Goptions.OptLocal -> true, false
+
+let remove_hints ~locality dbnames grs =
+  let local, superglobal = interp_locality locality in
   let dbnames = if List.is_empty dbnames then ["core"] else dbnames in
     List.iter
       (fun dbname ->
-        let hint = make_hint ~local dbname (RemoveHints grs) in
+        let hint = make_hint ~local dbname (RemoveHints { superglobal; hints = grs }) in
         Lib.add_anonymous_leaf (inAutoHint hint))
       dbnames
 
@@ -1185,11 +1207,6 @@ let remove_hints local dbnames grs =
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
 
-let check_no_export ~local ~superglobal () =
-  (* TODO: implement export for these entries *)
-  if not local && not superglobal then
-    CErrors.user_err Pp.(str "This command does not support the \"export\" attribute")
-
 let add_resolves env sigma clist ~local ~superglobal dbnames =
   List.iter
     (fun dbname ->
@@ -1229,27 +1246,24 @@ let add_unfolds l ~local ~superglobal dbnames =
     dbnames
 
 let add_cuts l ~local ~superglobal dbnames =
-  let () = check_no_export ~local ~superglobal () in
   List.iter
     (fun dbname ->
-      let hint = make_hint ~local dbname (AddCut l) in
+      let hint = make_hint ~local dbname (AddCut { superglobal; paths = l }) in
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_mode l m ~local ~superglobal dbnames =
-  let () = check_no_export ~local ~superglobal () in
   List.iter
     (fun dbname ->
       let m' = make_mode l m in
-      let hint = make_hint ~local dbname (AddMode (l, m')) in
+      let hint = make_hint ~local dbname (AddMode { superglobal; gref = l; mode = m' }) in
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_transparency l b ~local ~superglobal dbnames =
-  let () = check_no_export ~local ~superglobal () in
   List.iter
     (fun dbname ->
-      let hint = make_hint ~local dbname (AddTransparency (l, b)) in
+      let hint = make_hint ~local dbname (AddTransparency { superglobal; grefs = l; state = b }) in
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
@@ -1326,11 +1340,7 @@ let prepare_hint check env init (sigma,c) =
     (c', diff)
 
 let add_hints ~locality dbnames h =
-  let local, superglobal = match locality with
-  | Goptions.OptDefault | Goptions.OptGlobal -> false, true
-  | Goptions.OptExport -> false, false
-  | Goptions.OptLocal -> true, false
-  in
+  let local, superglobal = interp_locality locality in
   if String.List.mem "nocore" dbnames then
     user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
   assert (not (List.is_empty dbnames));
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 3d4d9c7970..54f4716652 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -189,7 +189,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit
 
 val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit
 
-val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit
+val remove_hints : locality:Goptions.option_locality -> hint_db_name list -> GlobRef.t list -> unit
 
 val current_db_names : unit -> String.Set.t
 
diff --git a/test-suite/output/HintLocality.out b/test-suite/output/HintLocality.out
new file mode 100644
index 0000000000..37a0613b25
--- /dev/null
+++ b/test-suite/output/HintLocality.out
@@ -0,0 +1,92 @@
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
diff --git a/test-suite/output/HintLocality.v b/test-suite/output/HintLocality.v
new file mode 100644
index 0000000000..4481335907
--- /dev/null
+++ b/test-suite/output/HintLocality.v
@@ -0,0 +1,72 @@
+(** Test hint command locality w.r.t. modules *)
+
+Create HintDb foodb.
+Create HintDb bardb.
+Create HintDb quxdb.
+
+#[global] Hint Immediate O : foodb.
+#[global] Hint Immediate O : bardb.
+#[global] Hint Immediate O : quxdb.
+
+Module Test.
+
+#[global] Hint Cut [ _ ] : foodb.
+#[global] Hint Mode S ! : foodb.
+#[global] Hint Opaque id : foodb.
+#[global] Remove Hints O : foodb.
+
+#[local] Hint Cut [ _ ] : bardb.
+#[local] Hint Mode S ! : bardb.
+#[local] Hint Opaque id : bardb.
+#[local] Remove Hints O : bardb.
+
+#[export] Hint Cut [ _ ] : quxdb.
+#[export] Hint Mode S ! : quxdb.
+#[export] Hint Opaque id : quxdb.
+#[export] Remove Hints O : quxdb.
+
+(** All three agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+End Test.
+
+(** bardb and quxdb agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+Import Test.
+
+(** foodb and quxdb agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+(** Test hint command locality w.r.t. sections *)
+
+Create HintDb secdb.
+
+#[global] Hint Immediate O : secdb.
+
+Section Sec.
+
+Fail #[global] Hint Cut [ _ ] : secdb.
+Fail #[global] Hint Mode S ! : secdb.
+Fail #[global] Hint Opaque id : secdb.
+Fail #[global] Remove Hints O : secdb.
+
+#[local] Hint Cut [ _ ] : secdb.
+#[local] Hint Mode S ! : secdb.
+#[local] Hint Opaque id : secdb.
+#[local] Remove Hints O : secdb.
+
+Print HintDb secdb.
+
+End Sec.
+
+Print HintDb secdb.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6a09250627..761f6ef5b7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1314,13 +1314,26 @@ let warn_implicit_core_hint_db =
          (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. "
              ++ strbrk"Please specify a hint database.")
 
-let vernac_remove_hints ~module_local dbnames ids =
+let check_hint_locality = function
+| OptGlobal ->
+  if Global.sections_are_opened () then
+  CErrors.user_err Pp.(str
+    "This command does not support the global attribute in sections.");
+| OptExport ->
+  if Global.sections_are_opened () then
+  CErrors.user_err Pp.(str
+    "This command does not support the export attribute in sections.");
+| OptDefault | OptLocal -> ()
+
+let vernac_remove_hints ~atts dbnames ids =
+  let locality = Attributes.(parse option_locality atts) in
+  let () = check_hint_locality locality in
   let dbnames =
     if List.is_empty dbnames then
       (warn_implicit_core_hint_db (); ["core"])
     else dbnames
   in
-  Hints.remove_hints module_local dbnames (List.map Smartlocate.global_with_alias ids)
+  Hints.remove_hints ~locality dbnames (List.map Smartlocate.global_with_alias ids)
 
 let vernac_hints ~atts dbnames h =
   let dbnames =
@@ -1329,17 +1342,7 @@ let vernac_hints ~atts dbnames h =
     else dbnames
   in
   let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in
-  let () = match locality with
-  | OptGlobal ->
-    if Global.sections_are_opened () then
-    CErrors.user_err Pp.(str
-      "This command does not support the global attribute in sections.");
-  | OptExport ->
-    if Global.sections_are_opened () then
-    CErrors.user_err Pp.(str
-      "This command does not support the export attribute in sections.");
-  | OptDefault | OptLocal -> ()
-  in
+  let () = check_hint_locality locality in
   Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x only_parsing =
@@ -2184,7 +2187,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
         with_module_locality ~atts vernac_create_hintdb dbname b)
   | VernacRemoveHints (dbnames,ids) ->
     VtDefault(fun () ->
-        with_module_locality ~atts vernac_remove_hints dbnames ids)
+        vernac_remove_hints ~atts dbnames ids)
   | VernacHints (dbnames,hints) ->
     VtDefault(fun () ->
         vernac_hints ~atts dbnames hints)