[string notation] Handle parameterized inductives and non inductives

11 files changed, 296 insertions, 218 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 60fbd68687..a52d7f08f0 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1386,7 +1386,7 @@ Scopes` or :cmd:`Print Scope`.
 ``char_scope``
   This scope includes interpretation for all strings of the form ``"c"``
   where :g:`c` is an ASCII character, or of the form ``"nnn"`` where nnn is
-  a three-digits number (possibly with leading 0's), or of the form
+  a three-digit number (possibly with leading 0s), or of the form
   ``""""``. Their respective denotations are the ASCII code of :g:`c`, the
   decimal ASCII code ``nnn``, or the ascii code of the character ``"`` (i.e.
   the ASCII code 34), all of them being represented in the type :g:`ascii`.
@@ -1556,13 +1556,13 @@ Number notations
 .. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print {? ( {+, @number_modifier } ) } : @scope_name
    :name: Number Notation
 
-   .. insertprodn number_modifier number_via
+   .. insertprodn number_modifier number_string_via
 
    .. prodn::
       number_modifier ::= warning after @bignat
       | abstract after @bignat
-      | @number_via
-      number_via ::= via @qualid mapping [ {+, {| @qualid => @qualid | [ @qualid ] => @qualid } } ]
+      | @number_string_via
+      number_string_via ::= via @qualid mapping [ {+, {| @qualid => @qualid | [ @qualid ] => @qualid } } ]
 
    This command allows the user to customize the way number literals
    are parsed and printed.
@@ -1608,11 +1608,7 @@ Number notations
          function application, constructors, inductive type families,
          sorts, and primitive integers) will be considered for printing.
 
-         .. note::
-            Number notations for parameterized inductive types can be
-            added by declaring an :ref:`abbreviation <Abbreviations>`
-            for the inductive which instantiates all parameters. See
-            example below.
+      .. _number-string-via:
 
       :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]`
          When using this option, :n:`@qualid__type` no
@@ -1649,22 +1645,6 @@ Number notations
             To use a :token:`sort` as the target type :n:`@qualid__type`, use an :ref:`abbreviation <Abbreviations>`
             as in the :ref:`example below <example-number-notation-non-inductive>`.
 
-         .. exn:: @qualid was already mapped to @qualid and cannot be remapped to @qualid
-
-            Duplicates are not allowed in the :n:`mapping` list.
-
-         .. exn:: Missing mapping for constructor @qualid
-
-            A mapping should be provided for :n:`@qualid` in the :n:`mapping` list.
-
-         .. warn:: @type was already mapped to @type, mapping it also to @type might yield ill typed terms when using the notation.
-
-            Two pairs in the :n:`mapping` list associate types that might be incompatible.
-
-         .. warn:: Type of @qualid seems incompatible with the type of @qualid. Expected type is: @type instead of @type. This might yield ill typed terms when using the notation.
-
-            A mapping given in the :n:`mapping` list associates a constant with a seemingly incompatible constructor.
-
       :n:`warning after @bignat`
          displays a warning message about a possible stack
          overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@bignat`.
@@ -1748,166 +1728,47 @@ Number notations
 
      At most one :g:`warning after` or :g:`abstract after` option can be given.
 
-   .. _example-number-notation-non-inductive:
-
-   .. example:: Number Notation for a non inductive type
-
-      The following example encodes the terms in the form :g:`sum unit ( ... (sum unit unit) ... )`
-      as the number of units in the term. For instance :g:`sum unit (sum unit unit)`
-      is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`.
-      The inductive :g:`I` will be used as :n:`@qualid__ind`.
-
-      .. coqtop:: in
-
-         Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I.
-
-      We then define :n:`@qualid__parse` and :n:`@qualid__print`
-
-      .. coqtop:: in
-
-         Definition of_uint (x : Number.uint) : I :=
-           let fix f n := match n with
-             | O => Iempty | S O => Iunit
-             | S n => Isum Iunit (f n) end in
-           f (Nat.of_num_uint x).
-
-         Definition to_uint (x : I) : Number.uint :=
-           let fix f i := match i with
-             | Iempty => O | Iunit => 1
-             | Isum i1 i2 => f i1 + f i2 end in
-           Nat.to_num_uint (f x).
-
-         Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B.
-
-      the number notation itself
-
-      .. coqtop:: in
-
-         Notation nSet := Set (only parsing).
-         Number Notation nSet of_uint to_uint (via I
-           mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) : type_scope.
-
-      and check the printer
-
-      .. coqtop:: all
-
-         Local Open Scope type_scope.
-         Check sum unit (sum unit unit).
-
-      and the parser
-
-      .. coqtop:: all
-
-         Set Printing All.
-         Check 3.
-
-   .. _example-number-notation-implicit-args:
-
-   .. example:: Number Notation with implicit arguments
-
-      The following example parses and prints natural numbers between
-      :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`.
-
-      .. coqtop:: all reset
-
-         Require Import Vector.
-         Print Fin.t.
-
-      Note the implicit arguments of :g:`Fin.F1` and :g:`Fin.FS`,
-      which won't appear in the corresponding inductive type.
-
-      .. coqtop:: in
-
-         Inductive I := I1 : I | IS : I -> I.
-
-         Definition of_uint (x : Number.uint) : I :=
-           let fix f n := match n with O => I1 | S n => IS (f n) end in
-           f (Nat.of_num_uint x).
-
-         Definition to_uint (x : I) : Number.uint :=
-           let fix f i := match i with I1 => O | IS n => S (f n) end in
-           Nat.to_num_uint (f x).
-
-         Declare Scope fin_scope.
-         Delimit Scope fin_scope with fin.
-         Local Open Scope fin_scope.
-         Number Notation Fin.t of_uint to_uint (via I
-           mapping [[Fin.F1] => I1, [Fin.FS] => IS]) : fin_scope.
-
-      Now :g:`2` is parsed as :g:`Fin.FS (Fin.FS Fin.F1)`, that is
-      :g:`@Fin.FS _ (@Fin.FS _ (@Fin.F1 _))`.
-
-      .. coqtop:: all
-
-         Check 2.
-
-      which can be of type :g:`Fin.t 3` (numbers :g:`0`, :g:`1` and :g:`2`)
-
-      .. coqtop:: all
-
-         Check 2 : Fin.t 3.
-
-      but cannot be of type :g:`Fin.t 2` (only :g:`0` and :g:`1`)
-
-      .. coqtop:: all fail
-
-         Check 2 : Fin.t 2.
-
-   .. example:: Number Notation with a parameterized inductive type
-
-      .. coqtop:: in reset
-
-         Definition of_uint u : list unit :=
-           let fix f n := match n with O => nil | S n => cons tt (f n) end in
-           f (Nat.of_num_uint u).
-         Definition to_uint (l : list unit) := Nat.to_num_uint (length l).
-
-      The parameter :g:`unit` for the parameterized inductive type
-      :g:`list` is given through an :ref:`abbreviation
-      <Abbreviations>`.
-
-      .. coqtop:: in
-
-         Notation list_unit := (list unit) (only parsing).
-         Number Notation list_unit of_uint to_uint : nat_scope.
-
 .. _string-notations:
 
 String notations
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: String Notation @qualid @qualid__parse @qualid__print : @scope_name
+.. cmd:: String Notation @qualid__type @qualid__parse @qualid__print {? ( @number_string_via ) } : @scope_name
    :name: String Notation
 
    Allows the user to customize how strings are parsed and printed.
 
-   The token :n:`@qualid` should be the name of an inductive type,
-   while :n:`@qualid__parse` and :n:`@qualid__print` should be the names of the
-   parsing and printing functions, respectively.  The parsing function
-   :n:`@qualid__parse` should have one of the following types:
+      :n:`@qualid__type`
+         the name of an inductive type,
+         while :n:`@qualid__parse` and :n:`@qualid__print` should be the names of the
+         parsing and printing functions, respectively.  The parsing function
+         :n:`@qualid__parse` should have one of the following types:
 
-      * :n:`Byte.byte -> @qualid`
-      * :n:`Byte.byte -> option @qualid`
-      * :n:`list Byte.byte -> @qualid`
-      * :n:`list Byte.byte -> option @qualid`
+            * :n:`Byte.byte -> @qualid__type`
+            * :n:`Byte.byte -> option @qualid__type`
+            * :n:`list Byte.byte -> @qualid__type`
+            * :n:`list Byte.byte -> option @qualid__type`
 
-   The printing function :n:`@qualid__print` should have one of the
-   following types:
+         The printing function :n:`@qualid__print` should have one of the
+         following types:
 
-      * :n:`@qualid -> Byte.byte`
-      * :n:`@qualid -> option Byte.byte`
-      * :n:`@qualid -> list Byte.byte`
-      * :n:`@qualid -> option (list Byte.byte)`
+            * :n:`@qualid__type -> Byte.byte`
+            * :n:`@qualid__type -> option Byte.byte`
+            * :n:`@qualid__type -> list Byte.byte`
+            * :n:`@qualid__type -> option (list Byte.byte)`
 
-   When parsing, the application of the parsing function
-   :n:`@qualid__parse` to the string will be fully reduced, and universes
-   of the resulting term will be refreshed.
+         When parsing, the application of the parsing function
+         :n:`@qualid__parse` to the string will be fully reduced, and universes
+         of the resulting term will be refreshed.
+
+         Note that only fully-reduced ground terms (terms containing only
+         function application, constructors, inductive type families,
+         sorts, and primitive integers) will be considered for printing.
 
-   Note that only fully-reduced ground terms (terms containing only
-   function application, constructors, inductive type families,
-   sorts, and primitive integers) will be considered for printing.
+      :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]`
+         works as for :ref:`number notations above <number-string-via>`.
 
-   .. exn:: Cannot interpret this string as a value of type @type
+  .. exn:: Cannot interpret this string as a value of type @type
 
      The string notation registered for :token:`type` does not support
      the given string.  This error is given when the interpretation
@@ -1926,7 +1787,7 @@ String notations
    .. exn:: Unexpected term @term while parsing a string notation.
 
      Parsing functions must always return ground terms, made up of
-     applications of constructors, inductive types, and primitive
+     function application, constructors, inductive type families, sorts and primitive
      integers.  Parsing functions may not return terms containing
      axioms, bare (co)fixpoints, lambdas, etc.
 
@@ -1937,12 +1798,33 @@ String notations
      concrete string expressed as a decimal.  They may not return
      opaque constants.
 
+.. note::
+   Number or string notations for parameterized inductive types can be
+   added by declaring an :ref:`abbreviation <Abbreviations>` for the
+   inductive which instantiates all parameters. See :ref:`example below <example-string-notation-parameterized-inductive>`.
+
 The following errors apply to both string and number notations:
 
    .. exn:: @type is not an inductive type.
 
      String and number notations can only be declared for inductive types.
-     Declare number notations for non-inductive types using :n:`@number_via`.
+     Declare string or numeral notations for non-inductive types using :n:`@number_string_via`.
+
+   .. exn:: @qualid was already mapped to @qualid and cannot be remapped to @qualid
+
+      Duplicates are not allowed in the :n:`mapping` list.
+
+   .. exn:: Missing mapping for constructor @qualid
+
+      A mapping should be provided for :n:`@qualid` in the :n:`mapping` list.
+
+   .. warn:: @type was already mapped to @type, mapping it also to @type might yield ill typed terms when using the notation.
+
+      Two pairs in the :n:`mapping` list associate types that might be incompatible.
+
+   .. warn:: Type of @qualid seems incompatible with the type of @qualid. Expected type is: @type instead of @type. This might yield ill typed terms when using the notation.
+
+      A mapping given in the :n:`mapping` list associates a constant with a seemingly incompatible constructor.
 
    .. exn:: Cannot interpret in @scope_name because @qualid could not be found in the current environment.
 
@@ -1975,6 +1857,129 @@ The following errors apply to both string and number notations:
 
      .. todo note on "single qualified identifiers" https://github.com/coq/coq/pull/11718#discussion_r415076703
 
+.. _example-number-notation-non-inductive:
+
+.. example:: Number Notation for a non inductive type
+
+   The following example encodes the terms in the form :g:`sum unit ( ... (sum unit unit) ... )`
+   as the number of units in the term. For instance :g:`sum unit (sum unit unit)`
+   is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`.
+   The inductive :g:`I` will be used as :n:`@qualid__ind`.
+
+   .. coqtop:: in
+
+      Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I.
+
+   We then define :n:`@qualid__parse` and :n:`@qualid__print`
+
+   .. coqtop:: in
+
+      Definition of_uint (x : Number.uint) : I :=
+        let fix f n := match n with
+          | O => Iempty | S O => Iunit
+          | S n => Isum Iunit (f n) end in
+        f (Nat.of_num_uint x).
+
+      Definition to_uint (x : I) : Number.uint :=
+        let fix f i := match i with
+          | Iempty => O | Iunit => 1
+          | Isum i1 i2 => f i1 + f i2 end in
+        Nat.to_num_uint (f x).
+
+      Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B.
+
+   the number notation itself
+
+   .. coqtop:: in
+
+      Notation nSet := Set (only parsing).
+      Number Notation nSet of_uint to_uint (via I
+        mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) : type_scope.
+
+   and check the printer
+
+   .. coqtop:: all
+
+      Local Open Scope type_scope.
+      Check sum unit (sum unit unit).
+
+   and the parser
+
+   .. coqtop:: all
+
+      Set Printing All.
+      Check 3.
+
+.. _example-number-notation-implicit-args:
+
+.. example:: Number Notation with implicit arguments
+
+   The following example parses and prints natural numbers between
+   :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`.
+
+   .. coqtop:: all reset
+
+      Require Import Vector.
+      Print Fin.t.
+
+   Note the implicit arguments of :g:`Fin.F1` and :g:`Fin.FS`,
+   which won't appear in the corresponding inductive type.
+
+   .. coqtop:: in
+
+      Inductive I := I1 : I | IS : I -> I.
+
+      Definition of_uint (x : Number.uint) : I :=
+        let fix f n := match n with O => I1 | S n => IS (f n) end in
+        f (Nat.of_num_uint x).
+
+      Definition to_uint (x : I) : Number.uint :=
+        let fix f i := match i with I1 => O | IS n => S (f n) end in
+        Nat.to_num_uint (f x).
+
+      Declare Scope fin_scope.
+      Delimit Scope fin_scope with fin.
+      Local Open Scope fin_scope.
+      Number Notation Fin.t of_uint to_uint (via I
+        mapping [[Fin.F1] => I1, [Fin.FS] => IS]) : fin_scope.
+
+   Now :g:`2` is parsed as :g:`Fin.FS (Fin.FS Fin.F1)`, that is
+   :g:`@Fin.FS _ (@Fin.FS _ (@Fin.F1 _))`.
+
+   .. coqtop:: all
+
+      Check 2.
+
+   which can be of type :g:`Fin.t 3` (numbers :g:`0`, :g:`1` and :g:`2`)
+
+   .. coqtop:: all
+
+      Check 2 : Fin.t 3.
+
+   but cannot be of type :g:`Fin.t 2` (only :g:`0` and :g:`1`)
+
+   .. coqtop:: all fail
+
+      Check 2 : Fin.t 2.
+
+.. _example-string-notation-parameterized-inductive:
+
+.. example:: String Notation with a parameterized inductive type
+
+   The parameter :g:`Byte.byte` for the parameterized inductive type
+   :g:`list` is given through an :ref:`abbreviation <Abbreviations>`.
+
+   .. coqtop:: in reset
+
+      Notation string := (list Byte.byte) (only parsing).
+      Definition id_string := @id string.
+
+      String Notation string id_string id_string : list_scope.
+
+   .. coqtop:: all
+
+      Check "abc"%list.
+
 .. _TacticNotation:
 
 Tactic Notations
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 "," "]"
 ]
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 1839e287d7..5f6fd62e5c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1107,11 +1107,12 @@ let coqbyte_of_string ?loc byte s =
   let p =
     if Int.equal (String.length s) 1 then int_of_char s.[0]
     else
-      if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
-      then int_of_string s
-      else
+      let n =
+        if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+        then int_of_string s else 256 in
+      if n < 256 then n else
        user_err ?loc ~hdr:"coqbyte_of_string"
-         (str "Expects a single character or a three-digits ascii code.") in
+         (str "Expects a single character or a three-digit ASCII code.") in
   coqbyte_of_char_code byte p
 
 let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c)
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
diff --git a/plugins/syntax/number.mli b/plugins/syntax/number.mli
index 5a13d1068b..d7d28b29ed 100644
--- a/plugins/syntax/number.mli
+++ b/plugins/syntax/number.mli
@@ -24,3 +24,8 @@ val vernac_number_notation : locality_flag ->
                              qualid -> qualid ->
                              number_option list ->
                              Notation_term.scope_name -> unit
+
+(** These are also used in string notations *)
+val locate_global_inductive : bool -> Libnames.qualid -> Names.inductive * Names.GlobRef.t option list
+val elaborate_to_post_params : Environ.env -> Evd.evar_map -> Names.inductive -> Names.GlobRef.t option list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list
+val elaborate_to_post_via : Environ.env -> Evd.evar_map -> Libnames.qualid -> Names.inductive -> (bool * Libnames.qualid * Libnames.qualid) list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index 98ea318c92..774d59dda3 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -14,15 +14,10 @@ open Libnames
 open Constrexpr
 open Constrexpr_ops
 open Notation
+open Number
 
 (** * String notation *)
 
-let get_constructors ind =
-  let mib,oib = Global.lookup_inductive ind in
-  let mc = oib.Declarations.mind_consnames in
-  Array.to_list
-    (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc)
-
 let qualid_of_ref n =
   n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
 
@@ -45,7 +40,7 @@ let type_error_of g ty =
     (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
      str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
 
-let vernac_string_notation local ty f g scope =
+let vernac_string_notation local ty f g via scope =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let app x y = mkAppC (x,[y]) in
@@ -55,14 +50,16 @@ let vernac_string_notation local ty f g scope =
   let coption = cref (q_option ()) in
   let opt r = app coption r in
   let clist_byte = app clist cbyte in
-  let tyc = Smartlocate.global_inductive_with_alias ty in
+  let ty_name = ty in
+  let ty, via =
+    match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in
+  let tyc, params = locate_global_inductive (via = None) ty in
   let to_ty = Smartlocate.global_with_alias f in
   let of_ty = Smartlocate.global_with_alias g in
   let cty = cref ty in
   let arrow x y =
     mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y)
   in
-  let constructors = get_constructors tyc in
   (* Check the type of f *)
   let to_kind =
     if has_type env sigma f (arrow clist_byte cty) then ListByte, Direct
@@ -79,12 +76,10 @@ let vernac_string_notation local ty f g scope =
     else if has_type env sigma g (arrow cty (opt cbyte)) then Byte, Option
     else type_error_of g ty
   in
-  let o = { to_kind = to_kind;
-            to_ty = to_ty;
-            to_post = [||];
-            of_kind = of_kind;
-            of_ty = of_ty;
-            ty_name = ty;
+  let to_post, pt_refs = match via with
+    | None -> elaborate_to_post_params env sigma tyc params
+    | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in
+  let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name;
             warning = () }
   in
   let i =
@@ -92,7 +87,7 @@ let vernac_string_notation local ty f g scope =
          pt_scope = scope;
          pt_interp_info = StringNotation o;
          pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
-         pt_refs = constructors;
+         pt_refs;
          pt_in_match = true }
   in
   enable_prim_token_interpretation i
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
index 0d99f98d26..f3c7c969c6 100644
--- a/plugins/syntax/string_notation.mli
+++ b/plugins/syntax/string_notation.mli
@@ -14,5 +14,7 @@ open Vernacexpr
 (** * String notation *)
 
 val vernac_string_notation : locality_flag ->
-                             qualid -> qualid -> qualid ->
+                             qualid ->
+                             qualid -> qualid ->
+                             Number.number_string_via option ->
                              Notation_term.scope_name -> unit
diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out
index e9cf4282dc..125c1bc927 100644
--- a/test-suite/output/StringSyntax.out
+++ b/test-suite/output/StringSyntax.out
@@ -1051,7 +1051,7 @@ Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
 "127"
      : byte
 The command has indeed failed with message:
-Expects a single character or a three-digits ascii code.
+Expects a single character or a three-digit ASCII code.
 "000"
      : ascii
 "a"
@@ -1059,7 +1059,7 @@ Expects a single character or a three-digits ascii code.
 "127"
      : ascii
 The command has indeed failed with message:
-Expects a single character or a three-digits ascii code.
+Expects a single character or a three-digit ASCII code.
 "000"
      : string
 "a"
@@ -1084,3 +1084,15 @@ Expects a single character or a three-digits ascii code.
      = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167";
        "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"]
      : list ascii
+"abc"
+     : string
+"000"
+     : nat
+"001"
+     : nat
+"002"
+     : nat
+"255"
+     : nat
+The command has indeed failed with message:
+Expects a single character or a three-digit ASCII code.
diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v
index aab6e0bb03..49584487a3 100644
--- a/test-suite/output/StringSyntax.v
+++ b/test-suite/output/StringSyntax.v
@@ -50,3 +50,48 @@ Local Close Scope byte_scope.
 Local Open Scope char_scope.
 Compute List.map Ascii.ascii_of_nat (List.seq 0 256).
 Local Close Scope char_scope.
+
+(* Test numeral notations for parameterized inductives *)
+Module Test2.
+
+Notation string := (list Byte.byte).
+Definition id_string := @id string.
+
+String Notation string id_string id_string : list_scope.
+
+Check "abc"%list.
+
+End Test2.
+
+(* Test the via ... using ... option *)
+Module Test3.
+
+Inductive I :=
+| IO : I
+| IS : I -> I.
+
+Definition of_byte (x : Byte.byte) : I :=
+  let fix f n :=
+      match n with
+      | O => IO
+      | S n => IS (f n)
+      end in
+  f (Byte.to_nat x).
+
+Definition to_byte (x : I) : option Byte.byte :=
+  let fix f i :=
+      match i with
+      | IO => O
+      | IS i => S (f i)
+      end in
+  Byte.of_nat (f x).
+
+String Notation nat of_byte to_byte (via I mapping [O => IO, S => IS]) : nat_scope.
+
+Check "000".
+Check "001".
+Check "002".
+Check "255".
+Fail Check "256".
+
+End Test3.