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

This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.

3 files changed, 25 insertions, 9 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 5d0f9208fc..4d615a130a 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 "Numeral" "Notation" reference reference reference ":" ident number_modifier
-| WITH "Numeral" "Notation" reference reference reference ":" scope_name number_modifier
-| REPLACE "Number" "Notation" reference reference reference ":" ident number_modifier
-| WITH "Number" "Notation" reference reference reference ":" scope_name number_modifier
+| 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 "String" "Notation" reference reference reference ":" ident
 | WITH "String" "Notation" reference reference reference ":" scope_name
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 914347b4cf..8a0feb0e2f 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 reference reference ":" ident number_modifier
-| "Numeral" "Notation" reference reference reference ":" ident number_modifier
+| "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier
+| "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier
 | "String" "Notation" reference reference reference ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr6      (* Ltac2 plugin *)
@@ -2555,6 +2555,14 @@ number_modifier: [
 | "(" "abstract" "after" bignat ")"
 ]
 
+number_using: [
+| reference reference
+]
+
+number_via: [
+| "via" reference "using" "(" LIST1 number_using SEP "," ")"
+]
+
 tac2pat1: [
 | Prim.qualid LIST1 tac2pat0      (* Ltac2 plugin *)
 | Prim.qualid      (* Ltac2 plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index a972ad4719..d12b3bf6cd 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -884,8 +884,8 @@ 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 number_modifier
-| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier
+| "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 +910,7 @@ 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 qualid qualid ":" scope_name OPT number_modifier
+| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT 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 ]
@@ -1275,6 +1275,14 @@ number_modifier: [
 | "(" "abstract" "after" bignat ")"
 ]
 
+number_using: [
+| qualid qualid
+]
+
+number_via: [
+| "via" qualid "using" "(" LIST1 number_using SEP "," ")"
+]
+
 hints_path: [
 | "(" hints_path ")"
 | hints_path "*"