Merge PR #12218: Numeral notations for non inductive types

Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48

4 files changed, 52 insertions, 20 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a143a6c7cf..97d479b238 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1285,12 +1285,12 @@ command: [
 | WITH "Declare" "Scope" scope_name
 
 (* odd that these are in command while other notation-related ones are in syntax *)
-| REPLACE "Numeral" "Notation" reference reference reference ":" ident numeral_modifier
-| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier
-| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier
-| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier
-| REPLACE "String" "Notation" reference reference reference ":" ident
-| WITH "String" "Notation" reference reference reference ":" scope_name
+| 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 OPT string_option ":" ident
+| WITH "String" "Notation" reference reference reference OPT string_option ":" scope_name
 
 | DELETE "Ltac2" ltac2_entry      (* was split up *)
 | DELETE "Add" "Zify" "InjTyp" constr      (* micromega plugin *)
@@ -1358,10 +1358,6 @@ explicit_subentry: [
 | DELETE "constr"    (* covered by another prod *)
 ]
 
-numeral_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
@@ -2465,6 +2461,9 @@ SPLICE: [
 | constr_with_bindings
 | simple_binding
 | ssexpr35 (* strange in mlg, ssexpr50 is after this *)
+| number_string_mapping
+| number_options
+| string_option
 ] (* end SPLICE *)
 
 RENAME: [
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index b7f1e18d2b..92bcd51528 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -538,12 +538,11 @@ let autoloaded_mlgs = [ (* in the order they are loaded by Coq *)
  "plugins/ltac/g_eqdecide.mlg";
  "plugins/ltac/g_tactic.mlg";
  "plugins/ltac/g_ltac.mlg";
- "plugins/syntax/g_string.mlg";
  "plugins/btauto/g_btauto.mlg";
  "plugins/rtauto/g_rtauto.mlg";
  "plugins/cc/g_congruence.mlg";
  "plugins/firstorder/g_ground.mlg";
- "plugins/syntax/g_numeral.mlg";
+ "plugins/syntax/g_number_string.mlg";
 ]
 
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 0638e1753b..20ac8f8bf3 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -686,9 +686,9 @@ command: [
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Number" "Notation" reference reference reference ":" ident numeral_modifier
-| "Numeral" "Notation" reference reference reference ":" ident numeral_modifier
-| "String" "Notation" reference reference reference ":" ident
+| "Number" "Notation" reference reference reference OPT number_options ":" ident
+| "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier
+| "String" "Notation" reference reference reference OPT string_option ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr6      (* Ltac2 plugin *)
 | "Print" "Ltac2" reference      (* Ltac2 plugin *)
@@ -2549,12 +2549,35 @@ field_mods: [
 | "(" LIST1 field_mod SEP "," ")"      (* ring plugin *)
 ]
 
-numeral_modifier: [
+deprecated_number_modifier: [
 |
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
 ]
 
+number_string_mapping: [
+| reference "=>" reference
+| "[" reference "]" "=>" reference
+]
+
+number_string_via: [
+| "via" reference "mapping" "[" LIST1 number_string_mapping SEP "," "]"
+]
+
+number_modifier: [
+| "warning" "after" bignat
+| "abstract" "after" bignat
+| number_string_via
+]
+
+number_options: [
+| "(" LIST1 number_modifier SEP "," ")"
+]
+
+string_option: [
+| "(" number_string_via ")"
+]
+
 tac2pat1: [
 | Prim.qualid LIST1 tac2pat0      (* Ltac2 plugin *)
 | Prim.qualid      (* Ltac2 plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 7d773e3a5b..75c0ca1453 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 qualid qualid ":" scope_name OPT numeral_modifier
-| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST1 qualid
 | "Typeclasses" "Opaque" LIST1 qualid
@@ -910,7 +908,9 @@ command: [
 | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family
 | "Declare" "Left" "Step" one_term
 | "Declare" "Right" "Step" one_term
-| "String" "Notation" qualid qualid qualid ":" scope_name
+| "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 OPT ( "(" number_string_via ")" ) ":" scope_name
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
 | assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
@@ -1269,11 +1269,22 @@ field_mod: [
 | "completeness" one_term      (* ring plugin *)
 ]
 
-numeral_modifier: [
+deprecated_number_modifier: [
+|
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
 ]
 
+number_modifier: [
+| "warning" "after" bignat
+| "abstract" "after" bignat
+| number_string_via
+]
+
+number_string_via: [
+| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]"
+]
+
 hints_path: [
 | "(" hints_path ")"
 | hints_path "*"