Separate interpretation of ltac definition and redefinition

This forbids redefinition in a mutual block (doesn't seem useful anyway)

doc/sphinx/proof-engine/ltac.rst

@@ -1911,6 +1911,8 @@ Defining |Ltac| symbols
       do not count as user-defined tactics for `::=`.  If :attr:`local` is not
       specified, the redefinition applies across module boundaries.
 
+      Redefinitions are incompatible with :n:`{* with @tacdef_body }`.
+
       .. exn:: There is no Ltac named @qualid
          :undocumented:
 

plugins/ltac/g_ltac.mlg

@@ -471,12 +471,12 @@ PRINTED BY { pr_tacdef_body env sigma }
 END
 
 VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
-| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
+| #[ raw_attributes; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
       | TacticRedefinition (qid,_) -> qualid_basename qid) l, VtLater)
   } -> {
-         Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l;
+         Tacentries.register_ltac raw_attributes l;
   }
 END
 

plugins/ltac/tacentries.ml

@@ -452,11 +452,6 @@ let create_ltac_quotation ~plugin name cast (e, l) =
 
 (** Command *)
 
-
-type tacdef_kind =
-  | NewTac of Id.t
-  | UpdateTac of Tacexpr.ltac_constant
-
 let is_defined_tac kn =
   try ignore (Tacenv.interp_ltac kn); true with Not_found -> false
 
@@ -465,40 +460,48 @@ let warn_unusable_identifier =
       (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++
         strbrk "may be unusable because of a conflict with a notation.")
 
-let register_ltac local ?deprecation tacl =
-  let map tactic_body =
-    match tactic_body with
+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 kn =
+    try Tacenv.locate_tactic qid
+    with Not_found ->
+      CErrors.user_err ?loc:qid.CAst.loc
+        (str "There is no Ltac named " ++ pr_qualid qid ++ str ".")
+  in
+  let ist = Tacintern.make_empty_glob_sign ~strict:true in
+  let body = Tacintern.intern_tactic_or_tacarg ist body in
+  Tacenv.redefine_ltac local kn body;
+  let name = Tacenv.shortest_qualid_of_tactic kn in
+  Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
+
+| tacl ->
+  let local, deprecation = Attributes.(parse Attributes.Notations.(locality ++ deprecation) atts) in
+  let local = Locality.make_module_locality local in
+  let map = function
     | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
-        let kn = Lib.make_kn id in
-        let id_pp = Id.print id in
-        let () = if is_defined_tac kn then
+      let kn = Lib.make_kn id in
+      let id_pp = Id.print id in
+      let () = if is_defined_tac kn then
           CErrors.user_err ?loc
             (str "There is already an Ltac named " ++ id_pp ++ str".")
-        in
-        let is_shadowed =
-          try
-            match Procq.parse_string Pltac.tactic (Id.to_string id) with
-            | { CAst.v=(Tacexpr.TacArg _) } -> false
-            | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
-          with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
-        in
-        let () = if is_shadowed then warn_unusable_identifier id in
-        NewTac id, body
+      in
+      let is_shadowed =
+        try
+          match Procq.parse_string Pltac.tactic (Id.to_string id) with
+          | { CAst.v=(Tacexpr.TacArg _) } -> false
+          | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
+        with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
+      in
+      let () = if is_shadowed then warn_unusable_identifier id in
+      id, body
     | Tacexpr.TacticRedefinition (qid, body) ->
-        let kn =
-          try Tacenv.locate_tactic qid
-          with Not_found ->
-            CErrors.user_err ?loc:qid.CAst.loc
-                       (str "There is no Ltac named " ++ pr_qualid qid ++ str ".")
-        in
-        UpdateTac kn, body
+      CErrors.user_err Pp.(str "Ltac redefinitions not supported in a mutual block.")
   in
   let rfun = List.map map tacl in
   let recvars =
-    let fold accu (op, _) = match op with
-    | UpdateTac _ -> accu
-    | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
-    in
+    let fold accu (id, _) = (Lib.make_path id, Lib.make_kn id) :: accu in
     List.fold_left fold [] rfun
   in
   let ist = Tacintern.make_empty_glob_sign ~strict:true in
@@ -517,15 +520,9 @@ let register_ltac local ?deprecation tacl =
   (* STATE XXX: Review what is going on here. Why does this needs
      protection? Why is not the STM level protection enough? Fishy *)
   let defs = Vernacstate.System.protect defs () in
-  let iter (def, tac) = match def with
-  | NewTac id ->
+  let iter (id, tac) =
     Tacenv.register_ltac false local id tac ?deprecation;
     Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
-  | UpdateTac kn ->
-    (* XXX if has_some deprecation then warn unsupported attribute? *)
-    Tacenv.redefine_ltac local kn tac;
-    let name = Tacenv.shortest_qualid_of_tactic kn in
-    Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
   in
   List.iter iter defs
 

plugins/ltac/tacentries.mli

@@ -15,8 +15,7 @@ open Tacexpr
 
 (** {5 Tactic Definitions} *)
 
-val register_ltac : locality_flag -> ?deprecation:Deprecation.t ->
-  Tacexpr.tacdef_body list -> unit
+val register_ltac : Attributes.vernac_flags -> Tacexpr.tacdef_body list -> unit
 (** Adds new Ltac definitions to the environment. *)
 
 (** {5 Tactic Notations} *)