Skip to content

Commit

Permalink
Remove the deprecated clear modifier.
Browse files Browse the repository at this point in the history
It has been deprecated since 8.17, long enough for people to have realized
this.
  • Loading branch information
ppedrot committed Apr 3, 2024
1 parent 17cde1a commit ff58952
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 9 deletions.
@@ -0,0 +1,4 @@
- **Removed:**
the clear modifier which was deprecated since 8.17
(`#18887 <https://github.com/coq/coq/pull/18887>`_,
by Pierre-Marie Pédrot).
10 changes: 1 addition & 9 deletions plugins/ltac/g_tactic.mlg
Expand Up @@ -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_
Expand Down Expand Up @@ -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) }
Expand Down

0 comments on commit ff58952

Please sign in to comment.