[numeral notation] Document the via ... using ... option

1 files changed, 16 insertions, 6 deletions

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 8a0feb0e2f..17fc220f6c 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -686,8 +686,8 @@ command: [
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier
-| "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier
+| "Number" "Notation" reference reference reference OPT number_options ":" ident
+| "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier
 | "String" "Notation" reference reference reference ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr6      (* Ltac2 plugin *)
@@ -2549,18 +2549,28 @@ field_mods: [
 | "(" LIST1 field_mod SEP "," ")"      (* ring plugin *)
 ]
 
-number_modifier: [
+deprecated_number_modifier: [
 |
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
 ]
 
-number_using: [
-| reference reference
+number_mapping: [
+| reference "=>" reference
 ]
 
 number_via: [
-| "via" reference "using" "(" LIST1 number_using SEP "," ")"
+| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]"
+]
+
+number_modifier: [
+| "warning" "after" bignat
+| "abstract" "after" bignat
+| number_via
+]
+
+number_options: [
+| "(" LIST1 number_modifier SEP "," ")"
 ]
 
 tac2pat1: [