From da4f6bcb4cc0b10a1ae2a368a66f1b09487ac058 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 1/2] 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 000000000000..faeccb705ec3 --- /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 450dd2b8e704..748fbf44d31f 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) } From c4e2ac04967202e82bbe6bea025724f77c45b73c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 4 Apr 2024 15:48:05 +0200 Subject: [PATCH 2/2] Fix grammar file. --- doc/tools/docgram/common.edit_mlg | 4 ---- doc/tools/docgram/fullGrammar | 1 - 2 files changed, 5 deletions(-) diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 2140445e0286..b651857600ea 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -2182,10 +2182,6 @@ cofixdecl: [ OPTINREF: [ ] -constr_with_bindings_arg: [ -| DELETE ">" constr_with_bindings -] - destruction_arg: [ | DELETE constr_with_bindings ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 4c9684fa4da8..ff6c26f74f2f 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -2364,7 +2364,6 @@ destruction_arg: [ ] constr_with_bindings_arg: [ -| ">" constr_with_bindings | constr_with_bindings ]