Hack a non-superglobal mode for hints.

The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.

10 files changed, 47 insertions, 46 deletions

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 82c64a9857..336c5a4bb0 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -249,7 +249,7 @@ 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)
+        Hints.add_hints ~local:(Locality.make_section_locality locality) ~superglobal:true
           (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..8b81b36fa2 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,7 @@ let remove_hints local dbnames grs =
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
-let add_resolves env sigma clist local dbnames =
+let add_resolves env sigma clist ~local ~superglobal dbnames =
   List.iter
     (fun dbname ->
       let r =
@@ -1190,14 +1197,14 @@ 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
 
@@ -1223,23 +1230,23 @@ let add_transparency l b local dbnames =
       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 +1410,22 @@ 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 ~local ~superglobal dbnames h =
   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
+  | 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 dbnames
   | HintsModeEntry (l,m) -> add_mode l m local dbnames
-  | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
+  | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames
   | HintsTransparencyEntry (lhints, b) ->
       add_transparency lhints b local 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..3fd4d6ea9e 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 : local:bool -> superglobal:bool -> 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/vernac/classes.ml b/vernac/classes.ml
index 16b9e07fb2..ee27a9f58b 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 superglobal = true in
+  Hints.add_hints ~local ~superglobal [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 ~local ~superglobal info poly =
      Flags.silently (fun () ->
-       Hints.add_hints ~local [typeclasses_db]
+       Hints.add_hints ~local ~superglobal [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
+  add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~local ~superglobal:true
     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))
+                ~local ~superglobal:true 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..527c6e24c8 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -123,7 +123,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 ~superglobal:false [Id.to_string prg.prg_name] (unfold_entry cst)
 
 (***********************************************************************)
 (* Saving an obligation                                                *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 27eb821a6a..7ce2d2a49c 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 ~local:true ~superglobal:false [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..be6ffa07b9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1180,7 +1180,7 @@ let vernac_hints ~atts dbnames h =
   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)
+  Hints.add_hints ~local ~superglobal:true 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