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

3 files changed, 31 insertions, 21 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4d615a130a..e43583de09 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1285,10 +1285,10 @@ command: [
 | WITH "Declare" "Scope" scope_name
 
 (* odd that these are in command while other notation-related ones are in syntax *)
-| REPLACE "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier
-| WITH "Number" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier
-| REPLACE "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier
-| WITH "Numeral" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier
+| REPLACE "Number" "Notation" reference reference reference OPT number_options ":" ident
+| WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name
+| REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier
+| WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier
 | REPLACE "String" "Notation" reference reference reference ":" ident
 | WITH "String" "Notation" reference reference reference ":" scope_name
 
@@ -1358,10 +1358,6 @@ explicit_subentry: [
 | DELETE "constr"    (* covered by another prod *)
 ]
 
-number_modifier: [
-| OPTINREF
-]
-
 binder_tactic: [
 | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5
 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5
@@ -2464,6 +2460,8 @@ SPLICE: [
 | constr_with_bindings
 | simple_binding
 | ssexpr35 (* strange in mlg, ssexpr50 is after this *)
+| number_mapping
+| number_options
 ] (* end SPLICE *)
 
 RENAME: [
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: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index d12b3bf6cd..3d1041e592 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -884,8 +884,6 @@ command: [
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Number" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier
-| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST1 qualid
 | "Typeclasses" "Opaque" LIST1 qualid
@@ -910,7 +908,8 @@ command: [
 | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
 | "Declare" "Left" "Step" one_term
 | "Declare" "Right" "Step" one_term
-| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier
+| "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name
+| "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier
 | "String" "Notation" qualid qualid qualid ":" scope_name
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
@@ -1270,17 +1269,20 @@ field_mod: [
 | "completeness" one_term      (* ring plugin *)
 ]
 
-number_modifier: [
+deprecated_number_modifier: [
+|
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
 ]
 
-number_using: [
-| qualid qualid
+number_modifier: [
+| "warning" "after" bignat
+| "abstract" "after" bignat
+| number_via
 ]
 
 number_via: [
-| "via" qualid "using" "(" LIST1 number_using SEP "," ")"
+| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]"
 ]
 
 hints_path: [