[string notation] Handle parameterized inductives and non inductives

3 files changed, 16 insertions, 11 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index e43583de09..5de1f09c53 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1289,8 +1289,8 @@ command: [
 | 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
+| 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 *)
@@ -2460,8 +2460,9 @@ SPLICE: [
 | constr_with_bindings
 | simple_binding
 | ssexpr35 (* strange in mlg, ssexpr50 is after this *)
-| number_mapping
+| number_string_mapping
 | number_options
+| string_option
 ] (* end SPLICE *)
 
 RENAME: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 3a0c3a8bc7..826a0b6f36 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -688,7 +688,7 @@ command: [
 | "Print" "Fields"      (* ring plugin *)
 | "Number" "Notation" reference reference reference OPT number_options ":" ident
 | "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier
-| "String" "Notation" reference reference reference ":" ident
+| "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 *)
@@ -2555,25 +2555,29 @@ deprecated_number_modifier: [
 | "(" "abstract" "after" bignat ")"
 ]
 
-number_mapping: [
+number_string_mapping: [
 | reference "=>" reference
 | "[" reference "]" "=>" reference
 ]
 
-number_via: [
-| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]"
+number_string_via: [
+| "via" reference "mapping" "[" LIST1 number_string_mapping SEP "," "]"
 ]
 
 number_modifier: [
 | "warning" "after" bignat
 | "abstract" "after" bignat
-| number_via
+| 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 13d8979208..151438bbbd 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -910,7 +910,7 @@ command: [
 | "Declare" "Right" "Step" one_term
 | "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
+| "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 ]
@@ -1278,10 +1278,10 @@ deprecated_number_modifier: [
 number_modifier: [
 | "warning" "after" bignat
 | "abstract" "after" bignat
-| number_via
+| number_string_via
 ]
 
-number_via: [
+number_string_via: [
 | "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]"
 ]