Implement export locality for the remaining Hint commands.

4 files changed, 79 insertions, 55 deletions

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/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 824bf35b1d..4988b2a100 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)