diff options
| author | Pierre Roux | 2020-09-09 23:33:05 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:23:24 +0200 |
| commit | 6551f14196784e323688e682877229bc7f901659 (patch) | |
| tree | 18fd2fd9da90095327498f0de309beb6d409c77a /plugins | |
| parent | d5eb564a1ae46409e90a2c6bd6af5b77aa37773e (diff) | |
Rename Numeral Notation command to Number Notation
Keep Numeral Notation wit a deprecation warning.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/syntax/g_numeral.mlg | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index e66dbe17b2..c030925ea9 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -24,6 +24,11 @@ let pr_numnot_option = function | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")" | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")" +let warn_deprecated_numeral_notation = + CWarnings.create ~name:"numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Numeral Notation is deprecated, please use Number Notation instead.") + } VERNAC ARGUMENT EXTEND numnotoption @@ -34,8 +39,13 @@ VERNAC ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) numnotoption(o) ] -> + + { warn_deprecated_numeral_notation (); + vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END |