[numeral notation] Handle implicit arguments

1 files changed, 9 insertions, 3 deletions

diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index e60ae45b01..a3cc786a4a 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -31,8 +31,13 @@ let warn_deprecated_numeral_notation =
     (fun () ->
       strbrk "Numeral Notation is deprecated, please use Number Notation instead.")
 
-let pr_number_mapping (n, n') =
-  Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () ++ Libnames.pr_qualid n'
+let pr_number_mapping (b, n, n') =
+  if b then
+    str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc ()
+    ++ Libnames.pr_qualid n'
+  else
+    Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc ()
+    ++ Libnames.pr_qualid n'
 
 let pr_number_via (n, l) =
   str "via " ++ Libnames.pr_qualid n ++ str " mapping ["
@@ -56,7 +61,8 @@ END
 
 VERNAC ARGUMENT EXTEND number_mapping
   PRINTED BY { pr_number_mapping }
-| [ reference(n) "=>" reference(n') ] -> { n, n' }
+| [ reference(n) "=>" reference(n') ] -> { false, n, n' }
+| [ "[" reference(n) "]" "=>" reference(n') ] -> { true, n, n' }
 END
 
 VERNAC ARGUMENT EXTEND number_via