[string notation] Handle parameterized inductives and non inductives

1 files changed, 20 insertions, 12 deletions

diff --git a/plugins/syntax/g_number_string.mlg b/plugins/syntax/g_number_string.mlg
index b584505530..c8badd238d 100644
--- a/plugins/syntax/g_number_string.mlg
+++ b/plugins/syntax/g_number_string.mlg
@@ -32,7 +32,7 @@ let warn_deprecated_numeral_notation =
     (fun () ->
       strbrk "Numeral Notation is deprecated, please use Number Notation instead.")
 
-let pr_number_mapping (b, n, n') =
+let pr_number_string_mapping (b, n, n') =
   if b then
     str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc ()
     ++ Libnames.pr_qualid n'
@@ -40,17 +40,20 @@ let pr_number_mapping (b, n, n') =
     Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc ()
     ++ Libnames.pr_qualid n'
 
-let pr_number_via (n, l) =
+let pr_number_string_via (n, l) =
   str "via " ++ Libnames.pr_qualid n ++ str " mapping ["
-  ++ prlist_with_sep pr_comma pr_number_mapping l ++ str "]"
+  ++ prlist_with_sep pr_comma pr_number_string_mapping l ++ str "]"
 
 let pr_number_modifier = function
   | After a -> pr_number_after a
-  | Via nl -> pr_number_via nl
+  | Via nl -> pr_number_string_via nl
 
 let pr_number_options l =
   str "(" ++ prlist_with_sep pr_comma pr_number_modifier l ++ str ")"
 
+let pr_string_option l =
+  str "(" ++ pr_number_string_via l ++ str ")"
+
 }
 
 VERNAC ARGUMENT EXTEND deprecated_number_modifier
@@ -60,22 +63,22 @@ VERNAC ARGUMENT EXTEND deprecated_number_modifier
 | [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) }
 END
 
-VERNAC ARGUMENT EXTEND number_mapping
-  PRINTED BY { pr_number_mapping }
+VERNAC ARGUMENT EXTEND number_string_mapping
+  PRINTED BY { pr_number_string_mapping }
 | [ reference(n) "=>" reference(n') ] -> { false, n, n' }
 | [ "[" reference(n) "]" "=>" reference(n') ] -> { true, n, n' }
 END
 
-VERNAC ARGUMENT EXTEND number_via
-  PRINTED BY { pr_number_via }
-| [ "via" reference(n) "mapping" "[" ne_number_mapping_list_sep(l, ",") "]" ] -> { n, l }
+VERNAC ARGUMENT EXTEND number_string_via
+  PRINTED BY { pr_number_string_via }
+| [ "via" reference(n) "mapping" "[" ne_number_string_mapping_list_sep(l, ",") "]" ] -> { n, l }
 END
 
 VERNAC ARGUMENT EXTEND number_modifier
   PRINTED BY { pr_number_modifier }
 | [ "warning" "after" bignat(waft) ] -> { After (Warning (NumTok.UnsignedNat.of_string waft)) }
 | [ "abstract" "after" bignat(n) ] -> { After (Abstract (NumTok.UnsignedNat.of_string n)) }
-| [ number_via(v) ] -> { Via v }
+| [ number_string_via(v) ] -> { Via v }
 END
 
 VERNAC ARGUMENT EXTEND number_options
@@ -83,6 +86,11 @@ VERNAC ARGUMENT EXTEND number_options
 | [ "(" ne_number_modifier_list_sep(l, ",") ")" ] -> { l }
 END
 
+VERNAC ARGUMENT EXTEND string_option
+  PRINTED BY { pr_string_option }
+| [ "(" number_string_via(v) ")" ] -> { v }
+END
+
 VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF
   | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) number_options_opt(nl) ":"
       ident(sc) ] ->
@@ -96,7 +104,7 @@ VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
-  | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
+  | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) string_option_opt(o) ":"
       ident(sc) ] ->
-    { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
+    { vernac_string_notation (Locality.make_module_locality locality) ty f g o (Id.to_string sc) }
 END