From 851e3dbb65ca9c83174f001cfb28595beb3d7ad4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 14 Jan 2025 17:55:32 +0100
Subject: [PATCH] Ltac redefinition support standard localities (default
 SuperGlobal)

Close #12206
---
 plugins/ltac/tacentries.ml |  7 +++++--
 plugins/ltac/tacenv.ml     | 18 ++++++++++++------
 plugins/ltac/tacenv.mli    |  5 ++---
 3 files changed, 19 insertions(+), 11 deletions(-)

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 550ca57d600b..2627c8cd66a6 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -462,8 +462,11 @@ let warn_unusable_identifier =
 
 let register_ltac atts = function
 | [Tacexpr.TacticRedefinition (qid, body)] ->
-  let local = Attributes.(parse locality atts) in
-  let local = Locality.make_module_locality local in
+  let local = Attributes.(parse explicit_hint_locality atts) in
+  let local = match local with
+    | Some local -> Locality.check_locality_nodischarge local; local
+    | None -> if Lib.sections_are_opened () then Local else SuperGlobal
+  in
   let kn =
     try Tacenv.locate_tactic qid
     with Not_found ->
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 7ffdaedfa99f..25378a0cb917 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -192,16 +192,22 @@ let register_ltac for_ml local ?deprecation id tac =
   Lib.add_leaf (inMD {local; id; for_ml; expr=tac; depr=deprecation})
 
 type tacreplace = {
-  repl_local : bool;
+  repl_local : Libobject.locality;
   repl_tac : ltac_constant;
   repl_expr : glob_tactic_expr;
 }
 
 let load_replace i (prefix, {repl_local; repl_tac; repl_expr=t}) =
-  replace repl_tac prefix.Nametab.obj_mp t
+  match repl_local with
+  | Local | Export -> ()
+  | SuperGlobal ->
+    replace repl_tac prefix.Nametab.obj_mp t
 
 let open_replace i (prefix, {repl_local; repl_tac; repl_expr=t}) =
-  replace repl_tac prefix.Nametab.obj_mp t
+  match repl_local with
+  | Local | SuperGlobal -> ()
+  | Export ->
+    replace repl_tac prefix.Nametab.obj_mp t
 
 let cache_replace (prefix, {repl_local; repl_tac; repl_expr=t}) =
   replace repl_tac prefix.Nametab.obj_mp t
@@ -212,9 +218,9 @@ let subst_replace (subst, {repl_local; repl_tac; repl_expr}) =
     repl_expr=Tacsubst.subst_tactic subst repl_expr;
   }
 
-let classify_replace = function
-  | {repl_local=false} -> Substitute
-  | {repl_local=true} -> Dispose
+let classify_replace o = match o.repl_local with
+  | Local -> Dispose
+  | Export | SuperGlobal -> Substitute
 
 let inReplace : tacreplace -> obj =
   declare_named_object_gen {(default_object "TAC-REDEFINITION") with
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index c525446e0fa7..a9d9749d3210 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -56,9 +56,8 @@ val register_ltac : bool -> bool -> ?deprecation:Deprecation.t -> Id.t ->
     definition. It also puts the Ltac name in the nametab, so that it can be
     used unqualified. *)
 
-val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit
-(** Replace a Ltac with the given name and body. If the boolean flag is set
-    to true, then this is a local redefinition. *)
+val redefine_ltac : Libobject.locality -> KerName.t -> glob_tactic_expr -> unit
+(** Replace a Ltac with the given name and body. *)
 
 val interp_ltac : KerName.t -> glob_tactic_expr
 (** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *)