Merge PR #11812: Add an Export locality to hints

Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: maximedenes

17 files changed, 153 insertions, 62 deletions

diff --git a/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh
new file mode 100644
index 0000000000..8dae29adb6
--- /dev/null
+++ b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11812" ] || [ "$CI_BRANCH" = "export-hint-globality" ]; then
+
+    equations_CI_REF="export-hint-globality"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    fiat_parsers_CI_REF="export-hint-globality"
+    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
+
+fi
diff --git a/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst
new file mode 100644
index 0000000000..9341eebb58
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  the :cmd:`Hint` commands now accept the :attr:`export` locality as
+  an attribute, allowing to make import-scoped hints
+  (`#11812 <https://github.com/coq/coq/pull/11812>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4f2f74aae4..be185e885b 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3759,6 +3759,24 @@ automatically created.
 .. cmd:: Hint @hint_definition : {+ @ident}
 
    The general command to add a hint to some databases :n:`{+ @ident}`.
+
+   This command supports the :attr:`local`, :attr:`global` and :attr:`export`
+   locality attributes. When no locality is explictly given, the
+   command is :attr:`local` inside a section and :attr:`global` otherwise.
+
+   + :attr:`local` hints are never visible from other modules, even if they
+     require or import the current module. Inside a section, the :attr:`local`
+     attribute is useless since hints do not survive anyway to the closure of
+     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.
+
+   + :attr:`global` hints are made available by merely requiring the current
+     module.
+
    The various possible :production:`hint_definition`\s are given below.
 
    .. cmdv:: Hint @hint_definition
@@ -3767,13 +3785,6 @@ automatically created.
 
       .. deprecated:: 8.10
 
-   .. cmdv:: Local Hint @hint_definition : {+ @ident}
-
-      This is used to declare hints that must not be exported to the other modules
-      that require and import the current module. Inside a section, the flag
-      Local is useless since hints do not survive anyway to the closure of
-      sections.
-
    .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident
       :name: Hint Resolve
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index d1f3dcc309..4401f8fa2f 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1190,6 +1190,12 @@ Controlling the locality of commands
      occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
      category.
 
+.. attr:: export
+
+  Some commands support an :attr:`export` attribute. The effect of the attribute
+  is to make the effect of the command available when the module containing it
+  is imported. The :cmd:`Hint` command accepts it for instance.
+
 .. _controlling-typing-flags:
 
 Controlling Typing Flags
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 82c64a9857..c43018022e 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -249,7 +249,8 @@ 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
-        Hints.add_hints ~local:(Locality.make_section_locality locality)
+        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;
  }
 END
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index aa2e96c2d7..d4f59d7a36 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -34,9 +34,6 @@ let get_typeclasses_unique_solutions =
     ~key:["Typeclasses";"Unique";"Solutions"]
     ~value:false
 
-let (set_typeclass_transparency, set_typeclass_transparency_hook) = Hook.make ()
-let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency gr local c
-
 let (classes_transparent_state, classes_transparent_state_hook) = Hook.make ()
 let classes_transparent_state () = Hook.get classes_transparent_state ()
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2715c1eda5..c350f97107 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -122,9 +122,6 @@ val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool ->
   ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
 val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr
 
-val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t
-val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
-
 val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t
 val classes_transparent_state : unit -> TransparentState.t
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e9ed43e3de..9c0cf03854 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1031,7 +1031,7 @@ let remove_hint dbname grs =
 type hint_action =
   | CreateDB of bool * TransparentState.t
   | AddTransparency of evaluable_global_reference hints_transparency_target * bool
-  | AddHints of hint_entry list
+  | AddHints of { superglobal : bool; hints : hint_entry list }
   | RemoveHints of GlobRef.t list
   | AddCut of hints_path
   | AddMode of GlobRef.t * hint_mode array
@@ -1057,14 +1057,21 @@ let load_autohint _ (kn, h) =
   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
-  | AddHints hints -> add_hint name hints
+  | 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
 
 let open_autohint i (kn, h) =
   if Int.equal i 1 then match h.hint_action with
-  | AddHints hints ->
+  | AddHints { superglobal; hints } ->
+    let () =
+      if not superglobal then
+        (* Import-bound hints must be declared when not imported yet *)
+        let filter (_, h) = not @@ KNmap.mem h.code.uid !statustable in
+        add_hint h.hint_name (List.filter filter hints)
+    in
     let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in
     List.iter add hints
   | _ -> ()
@@ -1133,9 +1140,9 @@ let subst_autohint (subst, obj) =
           else HintsReferences grs'
       in
       if target' == target then obj.hint_action else AddTransparency (target', b)
-    | AddHints hintlist ->
-      let hintlist' = List.Smart.map subst_hint hintlist in
-      if hintlist' == hintlist then obj.hint_action else AddHints hintlist'
+    | 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 ->
       let grs' = List.Smart.map (subst_global_reference subst) grs in
       if grs == grs' then obj.hint_action else RemoveHints grs'
@@ -1150,7 +1157,7 @@ let subst_autohint (subst, obj) =
 
 let classify_autohint obj =
   match obj.hint_action with
-  | AddHints [] -> Dispose
+  | AddHints { hints = [] } -> Dispose
   | _ -> if obj.hint_local then Dispose else Substitute obj
 
 let inAutoHint : hint_obj -> obj =
@@ -1182,7 +1189,13 @@ let remove_hints local dbnames grs =
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
-let add_resolves env sigma clist local dbnames =
+
+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 ->
       let r =
@@ -1190,25 +1203,27 @@ let add_resolves env sigma clist local dbnames =
           make_resolves env sigma (true,hnf,not !Flags.quiet)
             pri ~poly ~name:path gr) clist)
       in
-      let hint = make_hint ~local dbname (AddHints r) in
+      let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_unfolds l local dbnames =
+let add_unfolds l ~local ~superglobal dbnames =
   List.iter
     (fun dbname ->
-      let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in
+      let hint = make_hint ~local dbname (AddHints { superglobal; hints = List.map make_unfold l }) in
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_cuts l local 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
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_mode l m local 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
@@ -1216,30 +1231,31 @@ let add_mode l m local dbnames =
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_transparency l b local 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
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_extern info tacast local dbname =
+let add_extern info tacast ~local ~superglobal dbname =
   let pat = match info.hint_pattern with
   | None -> None
   | Some (_, pat) -> Some pat
   in
   let hint = make_hint ~local dbname
-                       (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
+                       (AddHints { superglobal; hints = [make_extern (Option.get info.hint_priority) pat tacast] }) in
   Lib.add_anonymous_leaf (inAutoHint hint)
 
-let add_externs info tacast local dbnames =
-  List.iter (add_extern info tacast local) dbnames
+let add_externs info tacast ~local ~superglobal dbnames =
+  List.iter (add_extern info tacast ~local ~superglobal) dbnames
 
-let add_trivials env sigma l local dbnames =
+let add_trivials env sigma l ~local ~superglobal dbnames =
   List.iter
     (fun dbname ->
       let l = List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l in
-      let hint = make_hint ~local dbname (AddHints l) in
+      let hint = make_hint ~local dbname (AddHints { superglobal; hints = l }) in
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
@@ -1403,22 +1419,27 @@ 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 dbnames h =
+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
   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));
   let env = Global.env() in
   let sigma = Evd.from_env env in
   match h with
-  | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
-  | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
-  | HintsCutEntry lhints -> add_cuts lhints local dbnames
-  | HintsModeEntry (l,m) -> add_mode l m local dbnames
-  | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
+  | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames
+  | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames
+  | HintsCutEntry lhints -> add_cuts lhints ~local ~superglobal dbnames
+  | HintsModeEntry (l,m) -> add_mode l m ~local ~superglobal dbnames
+  | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames
   | HintsTransparencyEntry (lhints, b) ->
-      add_transparency lhints b local dbnames
+      add_transparency lhints b ~local ~superglobal dbnames
   | HintsExternEntry (info, tacexp) ->
-      add_externs info tacexp local dbnames
+      add_externs info tacexp ~local ~superglobal dbnames
 
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 2663f65851..c9d4231d77 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -219,7 +219,7 @@ val current_pure_db : unit -> hint_db list
 
 val interp_hints : poly:bool -> hints_expr -> hints_entry
 
-val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
+val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
   env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t)
diff --git a/test-suite/success/export_hint.v b/test-suite/success/export_hint.v
new file mode 100644
index 0000000000..e18f7c1bef
--- /dev/null
+++ b/test-suite/success/export_hint.v
@@ -0,0 +1,22 @@
+Create HintDb foo.
+
+Module Foo.
+
+Axiom F : False.
+
+#[export]
+Hint Immediate F : foo.
+
+End Foo.
+
+Goal False.
+Proof.
+Fail solve [auto with foo].
+Abort.
+
+Import Foo.
+
+Goal False.
+Proof.
+auto with foo.
+Qed.
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 7213ba4829..96f126503d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -163,6 +163,16 @@ let program =
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
+let option_locality =
+  let name = "Locality" in
+  attribute_of_list [
+    ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal);
+    ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal);
+    ("export", single_key_parser ~name ~key:"export" Goptions.OptExport);
+  ] >>= function
+  | None -> return Goptions.OptDefault
+  | Some l -> return l
+
 let ukey = "universes"
 
 let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 7ecb7e4fb0..660652081f 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -47,6 +47,7 @@ val polymorphic : bool attribute
 val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
+val option_locality : Goptions.option_locality attribute
 val deprecation : Deprecation.t option attribute
 val canonical_field : bool attribute
 val canonical_instance : bool attribute
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 16b9e07fb2..99c92604ba 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -29,7 +29,8 @@ module NamedDecl = Context.Named.Declaration
 (*i*)
 
 let set_typeclass_transparency c local b =
-  Hints.add_hints ~local [typeclasses_db]
+  let locality = if local then Goptions.OptLocal else Goptions.OptGlobal in
+  Hints.add_hints ~locality [typeclasses_db]
     (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))
 
 let classes_transparent_state () =
@@ -38,12 +39,11 @@ let classes_transparent_state () =
   with Not_found -> TransparentState.empty
 
 let () =
-  Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
   Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state
 
-let add_instance_hint inst path local info poly =
+let add_instance_hint inst path ~locality info poly =
      Flags.silently (fun () ->
-       Hints.add_hints ~local [typeclasses_db]
+       Hints.add_hints ~locality [typeclasses_db]
           (Hints.HintsResolveEntry
              [info, poly, false, Hints.PathHints path, inst])) ()
 
@@ -55,16 +55,16 @@ let is_local_for_hint i =
                         add_instance_hint; don't ask hints to take discharge into account
                         itself *)
 
-let add_instance check inst =
+let add_instance_base inst =
   let poly = Global.is_polymorphic inst.is_impl in
-  let local = is_local_for_hint inst in
-  add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local
+  let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in
+  add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality
     inst.is_info poly;
   List.iter (fun (path, pri, c) ->
     let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in
     add_instance_hint h path
-                local pri poly)
-    (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
+                ~locality pri poly)
+    (build_subclasses ~check:(not (isVarRef inst.is_impl))
        (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
 
 let mk_instance cl info glob impl =
@@ -104,7 +104,7 @@ let discharge_instance (_, inst) =
 let is_local i = (i.is_global == None)
 
 let rebuild_instance inst =
-  add_instance true inst;
+  add_instance_base inst;
   inst
 
 let classify_instance inst =
@@ -124,7 +124,7 @@ let instance_input : instance -> obj =
 
 let add_instance i =
   Lib.add_anonymous_leaf (instance_input i);
-  add_instance true i
+  add_instance_base i
 
 let warning_not_a_class =
   let name = "not-a-class" in
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index eb9b896ec6..c973c84827 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -123,7 +123,8 @@ 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)
+  let locality = if local then Goptions.OptLocal else Goptions.OptExport in
+  Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst)
 
 (***********************************************************************)
 (* Saving an obligation                                                *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 27eb821a6a..dd90af0223 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -295,8 +295,8 @@ open Evd
 
 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)
+let add_local_hint prg cst =
+  Hints.add_hints ~locality:Goptions.OptLocal [Id.to_string prg.prg_name] (unfold_entry cst)
 
 let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind
                    notations obls impls ~scope ~poly ~kind reduce =
@@ -461,7 +461,7 @@ let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ }
       Univ.UContext.instance uctx, ctx'
   in
   let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
-  let () = if transparent then add_hint true prg cst in
+  let () = if transparent then add_local_hint prg cst in
   let obls = Array.copy obls in
   let () = obls.(num) <- obl in
   let prg = { prg with prg_ctx = ctx' } in
diff --git a/vernac/record.ml b/vernac/record.ml
index 065641989d..75e1088108 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -613,7 +613,7 @@ let add_constant_class env sigma cst =
     }
   in
   Classes.add_class env sigma tc;
-    set_typeclass_transparency (EvalConstRef cst) false false
+    Classes.set_typeclass_transparency (EvalConstRef cst) false false
 
 let add_inductive_class env sigma ind =
   let mind, oneind = Inductive.lookup_mind_specif env ind in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c78b470e3b..ba6d869589 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1178,9 +1178,19 @@ let vernac_hints ~atts dbnames h =
       (warn_implicit_core_hint_db (); ["core"])
     else dbnames
   in
-  let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
-  let local = enforce_module_locality local in
-  Hints.add_hints ~local dbnames (Hints.interp_hints ~poly h)
+  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
+  Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x only_parsing =
   let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in