diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 847e94c1a853..2780e9277fce 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/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: diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 362c38b6d889..dd8b9e2dd917 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/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 diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index faac267e391d..550ca57d600b 100644 --- a/plugins/ltac/tacentries.ml +++ b/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 diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index f2e40925137f..57e32ada4f05 100644 --- a/plugins/ltac/tacentries.mli +++ b/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} *)