From 6551f14196784e323688e682877229bc7f901659 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Wed, 9 Sep 2020 23:33:05 +0200
Subject: Rename Numeral Notation command to Number Notation

Keep Numeral Notation wit a deprecation warning.
---
 plugins/syntax/g_numeral.mlg | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'plugins/syntax')

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
-- 
cgit v1.2.3