diff options
| author | Michael Soegtrop | 2021-03-23 21:55:59 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2021-03-23 21:55:59 +0100 |
| commit | 47c20236f578dca9381822a62b5a406d6b42676d (patch) | |
| tree | fef686014dc1985799869ff1d6cab4e8f76ec8bc /user-contrib/Ltac2/g_ltac2.mlg | |
| parent | fa2ba1571cbd791c3b1acd87adeacd0aa4bd6e88 (diff) | |
| parent | 83c11db006ca87b3912d2548593b669884a3b4b5 (diff) | |
Merge PR #13774: Allow to register deprecation status in Ltac2 term and notation declarations
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'user-contrib/Ltac2/g_ltac2.mlg')
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 5297409cdf..4ef5c1a918 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -915,8 +915,8 @@ let classify_ltac2 = function } VERNAC COMMAND EXTEND VernacDeclareTactic2Definition -| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> { - Tac2entries.register_struct ?local e +| #[ deprecation = deprecation; local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> { + Tac2entries.register_struct ?deprecation ?local e } | ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> { fun ~pstate -> Tac2entries.perform_eval ~pstate e |