From 6016a980fa2ed33ff9bc49e6000436fe1ce6e260 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 22 Jun 2018 23:42:25 +0200 Subject: Tactic deprecation machinery We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.". --- CHANGES | 2 + .../language/gallina-specification-language.rst | 8 +++- grammar/tacextend.mlp | 6 ++- plugins/ltac/g_ltac.ml4 | 12 ++++-- plugins/ltac/tacentries.ml | 32 ++++++++------- plugins/ltac/tacentries.mli | 13 +++--- plugins/ltac/tacenv.ml | 47 ++++++++++++++-------- plugins/ltac/tacenv.mli | 18 +++++++-- plugins/ltac/tacexpr.ml | 4 +- plugins/ltac/tacexpr.mli | 4 +- plugins/ltac/tacintern.ml | 27 ++++++++++++- plugins/ltac/tacinterp.ml | 8 ++-- test-suite/output/Deprecation.out | 3 ++ test-suite/output/Deprecation.v | 6 +++ test-suite/success/LtacDeprecation.v | 32 +++++++++++++++ 15 files changed, 166 insertions(+), 56 deletions(-) create mode 100644 test-suite/output/Deprecation.out create mode 100644 test-suite/output/Deprecation.v create mode 100644 test-suite/success/LtacDeprecation.v diff --git a/CHANGES b/CHANGES index 6dce7b0db..fdd4feb59 100644 --- a/CHANGES +++ b/CHANGES @@ -38,6 +38,8 @@ Tactics without adding new ones. Preexisting tactic `constr_eq_nounivs` can still be used if you really want to ignore universe constraints. +- Tactics and tactic notations now understand the `deprecated` attribute. + Tools - Coq_makefile lets one override or extend the following variables from diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ac6a20198..8250b4b3d 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1430,6 +1430,12 @@ the following attributes names are recognized: Takes as value the optional attributes ``since`` and ``note``; both have a string value. + This attribute can trigger the following warnings: + + .. warn:: Tactic @qualid is deprecated since @string. @string. + + .. warn:: Tactic Notation @qualid is deprecated since @string. @string. + Here are a few examples: .. coqtop:: all reset @@ -1440,7 +1446,7 @@ Here are a few examples: exact O. Defined. - #[deprecated(since="8.9.0", note="use idtac instead")] + #[deprecated(since="8.9.0", note="Use idtac instead.")] Ltac foo := idtac. Goal True. diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index cea0bed59..02da61ef7 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -49,13 +49,17 @@ EXTEND GLOBAL: str_item; str_item: [ [ "TACTIC"; "EXTEND"; s = tac_name; + depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ]; level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ]; OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> let level = match level with Some i -> int_of_string i | None -> 0 in let level = mlexpr_of_int level in + let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in - declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ] + declare_str_items loc [ <:str_item< Tacentries.tactic_extend + $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation = + $depr$ } $l$ >> ] ] ] ; tacrule: [ [ "["; l = LIST1 tacargs; "]"; diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 9d86f21d4..c13bd69da 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -287,12 +287,14 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: - [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> + [ [ name = Constr.global; it=LIST1 input_fun; + redef = ltac_def_kind; body = tactic_expr -> if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in Tacexpr.TacticDefinition (id, TacFun (it, body)) - | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> + | name = Constr.global; redef = ltac_def_kind; + body = tactic_expr -> if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in @@ -468,7 +470,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in - Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; + let deprecation = atts.deprecated in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; st ] END @@ -512,7 +515,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in - Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; + let deprecation = atts.deprecated in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; st ] END diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index fac464a62..4b834d66d 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -252,7 +252,7 @@ type tactic_grammar_obj = { tacobj_key : KerName.t; tacobj_local : locality_flag; tacobj_tacgram : tactic_grammar; - tacobj_body : Id.t list * Tacexpr.glob_tactic_expr; + tacobj_body : Tacenv.alias_tactic; tacobj_forml : bool; } @@ -288,10 +288,11 @@ let load_tactic_notation i (_, tobj) = extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram let subst_tactic_notation (subst, tobj) = - let (ids, body) = tobj.tacobj_body in + let open Tacenv in + let alias = tobj.tacobj_body in { tobj with tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key; - tacobj_body = (ids, Tacsubst.subst_tactic subst body); + tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body }; } let classify_tactic_notation tacobj = Substitute tacobj @@ -308,25 +309,26 @@ let cons_production_parameter = function | TacTerm _ -> None | TacNonTerm (_, (_, ido)) -> ido -let add_glob_tactic_notation local ~level prods forml ids tac = +let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac = let parule = { tacgram_level = level; tacgram_prods = prods; } in + let open Tacenv in let tacobj = { tacobj_key = make_fresh_key prods; tacobj_local = local; tacobj_tacgram = parule; - tacobj_body = (ids, tac); + tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation }; tacobj_forml = forml; } in Lib.add_anonymous_leaf (inTacticGrammar tacobj) -let add_tactic_notation local n prods e = +let add_tactic_notation local n ?deprecation prods e = let ids = List.map_filter cons_production_parameter prods in let prods = List.map interp_prod_item prods in let tac = Tacintern.glob_tactic_env ids (Global.env()) e in - add_glob_tactic_notation local ~level:n prods false ids tac + add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac (**********************************************************************) (* ML Tactic entries *) @@ -366,7 +368,7 @@ let extend_atomic_tactic name entries = in List.iteri add_atomic entries -let add_ml_tactic_notation name ~level prods = +let add_ml_tactic_notation name ~level ?deprecation prods = let len = List.length prods in let iter i prods = let open Tacexpr in @@ -378,7 +380,7 @@ let add_ml_tactic_notation name ~level prods = let entry = { mltac_name = name; mltac_index = len - i - 1 } in let map id = Reference (Locus.ArgVar (CAst.make id)) in let tac = TacML (Loc.tag (entry, List.map map ids)) in - add_glob_tactic_notation false ~level prods true ids tac + add_glob_tactic_notation false ~level ?deprecation prods true ids tac in List.iteri iter (List.rev prods); (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at @@ -430,7 +432,7 @@ 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 tacl = +let register_ltac local ?deprecation tacl = let map tactic_body = match tactic_body with | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) -> @@ -483,10 +485,10 @@ let register_ltac local tacl = let defs = States.with_state_protection defs () in let iter (def, tac) = match def with | NewTac id -> - Tacenv.register_ltac false local id tac; + Tacenv.register_ltac false local id tac ?deprecation; Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") | UpdateTac kn -> - Tacenv.redefine_ltac local kn tac; + Tacenv.redefine_ltac local kn tac ?deprecation; let name = Tacenv.shortest_qualid_of_tactic kn in Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined") in @@ -658,7 +660,7 @@ let lift_constr_tac_to_ml_tac vars tac = end in tac -let tactic_extend plugin_name tacname ~level sign = +let tactic_extend plugin_name tacname ~level ?deprecation sign = let open Tacexpr in let ml_tactic_name = { mltac_tactic = tacname; @@ -687,10 +689,10 @@ let tactic_extend plugin_name tacname ~level sign = This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in let id = Names.Id.of_string name in - let obj () = Tacenv.register_ltac true false id body in + let obj () = Tacenv.register_ltac true false id body ?deprecation in let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in Mltop.declare_cache_obj obj plugin_name | _ -> - let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in + let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); Mltop.declare_cache_obj obj plugin_name diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index f873631ff..138a584e0 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -12,10 +12,12 @@ open Vernacexpr open Tacexpr +open Vernacinterp (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit +val register_ltac : locality_flag -> ?deprecation:deprecation -> + Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) (** {5 Tactic Notations} *) @@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol leaves. *) val add_tactic_notation : - locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list -> - raw_tactic_expr -> unit + locality_flag -> int -> ?deprecation:deprecation -> raw_argument + grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit (** [add_tactic_notation local level prods expr] adds a tactic notation in the environment at level [level] with locality [local] made of the grammar productions [prods] and returning the body [expr] *) @@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type - to finding an argument by name (as in {!Genarg}) if there is none matching. *) -val add_ml_tactic_notation : ml_tactic_name -> level:int -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation -> argument grammar_tactic_prod_item_expr list list -> unit (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND ML-side macro. *) @@ -78,4 +80,5 @@ type _ ty_sig = type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml -val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit +val tactic_extend : string -> string -> level:Int.t -> + ?deprecation:deprecation -> ty_ml list -> unit diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index d5ab2d690..0bb9ccb1d 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -52,7 +52,11 @@ let shortest_qualid_of_tactic kn = (** Tactic notations (TacAlias) *) type alias = KerName.t -type alias_tactic = Id.t list * glob_tactic_expr +type alias_tactic = + { alias_args: Id.t list; + alias_body: glob_tactic_expr; + alias_deprecation: Vernacinterp.deprecation option; + } let alias_map = Summary.ref ~name:"tactic-alias" (KNmap.empty : alias_tactic KNmap.t) @@ -118,6 +122,7 @@ type ltac_entry = { tac_for_ml : bool; tac_body : glob_tactic_expr; tac_redef : ModPath.t list; + tac_deprecation : Vernacinterp.deprecation option } let mactab = @@ -130,8 +135,12 @@ let interp_ltac r = (KNmap.find r !mactab).tac_body let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml -let add kn b t = - let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in +let add ~deprecation kn b t = + let entry = { tac_for_ml = b; + tac_body = t; + tac_redef = []; + tac_deprecation = deprecation; + } in mactab := KNmap.add kn entry !mactab let replace kn path t = @@ -139,34 +148,38 @@ let replace kn path t = let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in mactab := KNmap.modify kn entry !mactab -let load_md i ((sp, kn), (local, id, b, t)) = match id with +let tac_deprecation kn = + try (KNmap.find kn !mactab).tac_deprecation with Not_found -> None + +let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> let () = if not local then push_tactic (Until i) sp kn in - add kn b t + add ~deprecation kn b t | Some kn0 -> replace kn0 kn t -let open_md i ((sp, kn), (local, id, b, t)) = match id with +let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> let () = if not local then push_tactic (Exactly i) sp kn in - add kn b t + add ~deprecation kn b t | Some kn0 -> replace kn0 kn t -let cache_md ((sp, kn), (local, id ,b, t)) = match id with +let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with | None -> let () = push_tactic (Until 1) sp kn in - add kn b t + add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let subst_kind subst id = match id with | None -> None | Some kn -> Some (Mod_subst.subst_kn subst kn) -let subst_md (subst, (local, id, b, t)) = - (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t) +let subst_md (subst, (local, id, b, t, deprecation)) = + (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t, deprecation) -let classify_md (local, _, _, _ as o) = Substitute o +let classify_md (local, _, _, _, _ as o) = Substitute o -let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = +let inMD : bool * ltac_constant option * bool * glob_tactic_expr * + Vernacinterp.deprecation option -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; @@ -174,8 +187,8 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = subst_function = subst_md; classify_function = classify_md} -let register_ltac for_ml local id tac = - ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac))) +let register_ltac for_ml local ?deprecation id tac = + ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac, deprecation))) -let redefine_ltac local kn tac = - Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac)) +let redefine_ltac local ?deprecation kn tac = + Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac, deprecation)) diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 3af2f2a46..7143f5185 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -12,6 +12,7 @@ open Names open Libnames open Tacexpr open Geninterp +open Vernacinterp (** This module centralizes the various ways of registering tactics. *) @@ -29,7 +30,11 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid type alias = KerName.t (** Type of tactic alias, used in the [TacAlias] node. *) -type alias_tactic = Id.t list * glob_tactic_expr +type alias_tactic = + { alias_args: Id.t list; + alias_body: glob_tactic_expr; + alias_deprecation: Vernacinterp.deprecation option; + } (** Contents of a tactic notation *) val register_alias : alias -> alias_tactic -> unit @@ -43,7 +48,8 @@ val check_alias : alias -> bool (** {5 Coq tactic definitions} *) -val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit +val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> + glob_tactic_expr -> unit (** Register a new Ltac with the given name and body. The first boolean indicates whether this is done from ML side, rather than @@ -51,7 +57,8 @@ val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit 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 +val redefine_ltac : bool -> ?deprecation:deprecation -> 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. *) @@ -61,6 +68,9 @@ val interp_ltac : KerName.t -> glob_tactic_expr val is_ltac_for_ml_tactic : KerName.t -> bool (** Whether the tactic is defined from ML-side *) +val tac_deprecation : KerName.t -> deprecation option +(** The tactic deprecation notice, if any *) + type ltac_entry = { tac_for_ml : bool; (** Whether the tactic is defined from ML-side *) @@ -68,6 +78,8 @@ type ltac_entry = { (** The current body of the tactic *) tac_redef : ModPath.t list; (** List of modules redefining the tactic in reverse chronological order *) + tac_deprecation : deprecation option; + (** Deprecation notice to be printed when the tactic is used *) } val ltac_entries : unit -> ltac_entry KNmap.t diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 06d2711ad..59b748e25 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -398,5 +398,5 @@ type ltac_call_kind = type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = - | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 71e1edfd7..3a0badb28 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -398,5 +398,5 @@ type ltac_call_kind = type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = - | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 481fc30df..144480062 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -117,9 +117,26 @@ let intern_constr_reference strict ist qid = (* Internalize an isolated reference in position of tactic *) +let warn_deprecated_tactic = + CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated" + (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++ + strbrk " is deprecated" ++ + pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++ + str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note) + +let warn_deprecated_alias = + CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated" + (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++ + strbrk " is deprecated since" ++ + pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++ + str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note) + let intern_isolated_global_tactic_reference qid = let loc = qid.CAst.loc in - TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) + let kn = Tacenv.locate_tactic qid in + Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@ + Tacenv.tac_deprecation kn; + TacCall (Loc.tag ?loc (ArgArg (loc,kn),[])) let intern_isolated_tactic_reference strict ist qid = (* An ltac reference *) @@ -137,7 +154,11 @@ let intern_isolated_tactic_reference strict ist qid = (* Internalize an applied tactic reference *) let intern_applied_global_tactic_reference qid = - ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid) + let loc = qid.CAst.loc in + let kn = Tacenv.locate_tactic qid in + Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@ + Tacenv.tac_deprecation kn; + ArgArg (loc,kn) let intern_applied_tactic_reference ist qid = (* An ltac reference *) @@ -643,6 +664,8 @@ and intern_tactic_seq onlytac ist = function (* For extensions *) | TacAlias (loc,(s,l)) -> + let alias = Tacenv.interp_alias s in + Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation; let l = List.map (intern_tacarg !strict_check false ist) l in ist.ltacvars, TacAlias (Loc.tag ?loc (s,l)) | TacML (loc,(opn,l)) -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index d9ac96d89..77b5b06d4 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1125,17 +1125,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias (loc,(s,l)) -> - let (ids, body) = Tacenv.interp_alias s in + let alias = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in let tac l = let addvar x v accu = Id.Map.add x v accu in - let lfun = List.fold_right2 addvar ids l ist.lfun in + let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace -> let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in - val_interp ist body >>= fun v -> + val_interp ist alias.Tacenv.alias_body >>= fun v -> Ftactic.lift (tactic_of_value ist v) in let tac = @@ -1147,7 +1147,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with some more elaborate solution will have to be used. *) in let tac = - let len1 = List.length ids in + let len1 = List.length alias.Tacenv.alias_args in let len2 = List.length l in if len1 = len2 then tac else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \ diff --git a/test-suite/output/Deprecation.out b/test-suite/output/Deprecation.out new file mode 100644 index 000000000..7e290847c --- /dev/null +++ b/test-suite/output/Deprecation.out @@ -0,0 +1,3 @@ +File "stdin", line 5, characters 0-3: +Warning: Tactic foo is deprecated since X.Y. Use idtac instead. +[deprecated-tactic,deprecated] diff --git a/test-suite/output/Deprecation.v b/test-suite/output/Deprecation.v new file mode 100644 index 000000000..04d5eb3d4 --- /dev/null +++ b/test-suite/output/Deprecation.v @@ -0,0 +1,6 @@ +#[deprecated(since = "X.Y", note = "Use idtac instead.")] + Ltac foo := idtac. + +Goal True. +foo. +Abort. diff --git a/test-suite/success/LtacDeprecation.v b/test-suite/success/LtacDeprecation.v new file mode 100644 index 000000000..633a5e474 --- /dev/null +++ b/test-suite/success/LtacDeprecation.v @@ -0,0 +1,32 @@ +Set Warnings "+deprecated". + +#[deprecated(since = "8.8", note = "Use idtac instead")] +Ltac foo x := idtac. + +Goal True. +Fail (foo true). +Abort. + +Fail Ltac bar := foo. +Fail Tactic Notation "bar" := foo. + +#[deprecated(since = "8.8", note = "Use idtac instead")] +Tactic Notation "bar" := idtac. + +Goal True. +Fail bar. +Abort. + +Fail Ltac zar := bar. + +Set Warnings "-deprecated". + +Ltac zar := foo. +Ltac zarzar := bar. + +Set Warnings "+deprecated". + +Goal True. +zar x. +zarzar. +Abort. -- cgit v1.2.3