From ff58952439b095006749bee71f6877e470aca08e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 3 Apr 2024 13:14:02 +0200 Subject: [PATCH] Remove the deprecated clear modifier. It has been deprecated since 8.17, long enough for people to have realized this. --- .../04-tactics/18887-rm-deprecated-clear-modifier.rst | 4 ++++ plugins/ltac/g_tactic.mlg | 10 +--------- 2 files changed, 5 insertions(+), 9 deletions(-) create mode 100644 doc/changelog/04-tactics/18887-rm-deprecated-clear-modifier.rst diff --git a/doc/changelog/04-tactics/18887-rm-deprecated-clear-modifier.rst b/doc/changelog/04-tactics/18887-rm-deprecated-clear-modifier.rst new file mode 100644 index 0000000000000..faeccb705ec35 --- /dev/null +++ b/doc/changelog/04-tactics/18887-rm-deprecated-clear-modifier.rst @@ -0,0 +1,4 @@ +- **Removed:** + the clear modifier which was deprecated since 8.17 + (`#18887 `_, + by Pierre-Marie Pédrot). diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 450dd2b8e7044..748fbf44d31fd 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -198,11 +198,6 @@ let deprecated_conversion_at_with = ~name:"conversion_at_with" ~category:Deprecation.Version.v8_14 (fun () -> Pp.str "The syntax [at ... with ...] is deprecated. Use [with ... at ...] instead.") -let deprecated_clear_modifier = - CWarnings.create - ~name:"deprecated-clear-modifier" ~category:Deprecation.Version.v8_17 - (fun () -> Pp.strbrk "The undocumented clear modifier \">\" is deprecated. Open an issue at https://github.com/coq/coq/issues/new if you actually depend on this feature in your work.") - (* Auxiliary grammar rules *) open Pvernac.Vernac_ @@ -240,10 +235,7 @@ GRAMMAR EXTEND Gram ] ] ; constr_with_bindings_arg: - [ [ ">"; c = constr_with_bindings -> - { deprecated_clear_modifier (); (* 8.17 *) - (Some true,c) } - | c = constr_with_bindings -> { (None,c) } ] ] + [ [ c = constr_with_bindings -> { (None,c) } ] ] ; quantified_hypothesis: [ [ id = ident -> { NamedHyp (CAst.make ~loc id) }