Support locality attributes for Hint Rewrite (including export)

We deprecate unspecified locality as was done for Hint.

Close #13724

4 files changed, 41 insertions, 6 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index cc56de066d..1d876537ef 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -206,9 +206,15 @@ let subst_hintrewrite (subst,(rbase,list as node)) =
       (rbase,list')
 
 (* Declaration of the Hint Rewrite library object *)
-let inHintRewrite : string * HintDN.t -> Libobject.obj =
+let inGlobalHintRewrite : string * HintDN.t -> Libobject.obj =
   let open Libobject in
-  declare_object @@ superglobal_object_nodischarge "HINT_REWRITE"
+  declare_object @@ superglobal_object_nodischarge "HINT_REWRITE_GLOBAL"
+    ~cache:cache_hintrewrite
+    ~subst:(Some subst_hintrewrite)
+
+let inExportHintRewrite : string * HintDN.t -> Libobject.obj =
+  let open Libobject in
+  declare_object @@ global_object_nodischarge "HINT_REWRITE_EXPORT"
     ~cache:cache_hintrewrite
     ~subst:(Some subst_hintrewrite)
 
@@ -250,7 +256,8 @@ let find_applied_relation ?loc env sigma c left2right =
                        spc () ++ str"of this term does not end with an applied relation.")
 
 (* To add rewriting rules to a base *)
-let add_rew_rules base lrul =
+let add_rew_rules ~locality base lrul =
+  let () = Hints.check_hint_locality locality in
   let counter = ref 0 in
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -267,5 +274,9 @@ let add_rew_rules base lrul =
                     rew_tac = Option.map intern t}
         in incr counter;
           HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
-  in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
-
+  in
+  let open Goptions in
+  match locality with
+  | OptLocal -> cache_hintrewrite ((),(base,lrul))
+  | OptDefault | OptGlobal -> Lib.add_anonymous_leaf (inGlobalHintRewrite (base,lrul))
+  | OptExport -> Lib.add_anonymous_leaf (inExportHintRewrite (base,lrul))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 974aef8e8f..dec6cc5ef4 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -17,7 +17,7 @@ open Equality
 type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) CAst.t
 
 (** To add rewriting rules to a base *)
-val add_rew_rules : string -> raw_rew_rule list -> unit
+val add_rew_rules : locality:Goptions.option_locality -> string -> raw_rew_rule list -> unit
 
 (** The AutoRewrite tactic.
    The optional conditions tell rewrite how to handle matching and side-condition solving.
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0cc8becd8f..058602acfd 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1187,6 +1187,28 @@ 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 warn_deprecated_hint_without_locality =
+  CWarnings.create ~name:"deprecated-hint-without-locality" ~category:"deprecated"
+    (fun () -> strbrk "The default value for hint locality is currently \
+    \"local\" in a section and \"global\" otherwise, but is scheduled to change \
+    in a future release. For the time being, adding hints outside of sections \
+    without specifying an explicit locality is therefore deprecated. It is \
+    recommended to use \"export\" whenever possible.")
+
+let check_hint_locality = let open Goptions in 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 ->
+  if not @@ Global.sections_are_opened () then
+    warn_deprecated_hint_without_locality ()
+| OptLocal -> ()
+
 let interp_locality = function
 | Goptions.OptDefault | Goptions.OptGlobal -> false, true
 | Goptions.OptExport -> false, false
diff --git a/tactics/hints.mli b/tactics/hints.mli
index f5947bb946..381c7a1951 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -182,6 +182,8 @@ val searchtable_map : hint_db_name -> hint_db
 
 val searchtable_add : (hint_db_name * hint_db) -> unit
 
+val check_hint_locality : Goptions.option_locality -> unit
+
 (** [create_hint_db local name st use_dn].
    [st] is a transparency state for unification using this db
    [use_dn] switches the use of the discrimination net for all hints