Ltac redefinition support standard localities (default SuperGlobal)

Close coq#12206

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 ->

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

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. *)