Better primitive type support in custom string and numeral notations.

- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API)
- the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors
- Grants #13484: String notations for primitive arrays
- Fixes #13517: String notation printing fails with primitive integers inside lists

1 files changed, 4 insertions, 2 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index df73de846f..094a98e225 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1734,7 +1734,8 @@ Number notations
 
          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.
+         sorts, primitive integers, primitive floats, primitive arrays and type
+         constants for primitive types) will be considered for printing.
 
       .. _number-string-via:
 
@@ -1891,7 +1892,8 @@ String notations
 
          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.
+         sorts, primitive integers, primitive floats, primitive arrays and type
+         constants for primitive types) will be considered for printing.
 
       :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]`
          works as for :ref:`number notations above <number-string-via>`.