Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into multiple pages.

Reviewed-by: jfehrle

1 files changed, 23 insertions, 2 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 60cd4c4ad8..955f2055e4 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1429,10 +1429,31 @@ Abbreviations
       Notation F p P := (force2 p (fun p => P)).
       Check exists x y, F (x,y) (x >= 1 /\ y >= 2).
 
+.. extracted from Gallina chapter
+
+Numerals and strings
+--------------------
+
+.. insertprodn primitive_notations primitive_notations
+
+.. prodn::
+   primitive_notations ::= @numeral
+   | @string
+
+Numerals and strings have no predefined semantics in the calculus. They are
+merely notations that can be bound to objects through the notation mechanism.
+Initially, numerals are bound to Peano’s representation of natural
+numbers (see :ref:`datatypes`).
+
+.. note::
+
+   Negative integers are not at the same level as :n:`@num`, for this
+   would make precedence unnatural.
+
 .. _numeral-notations:
 
 Numeral notations
------------------
+~~~~~~~~~~~~~~~~~
 
 .. cmd:: Numeral Notation @qualid @qualid__parse @qualid__print : @scope_name {? @numeral_modifier }
    :name: Numeral Notation
@@ -1557,7 +1578,7 @@ Numeral notations
      opaque constants.
 
 String notations
------------------
+~~~~~~~~~~~~~~~~
 
 .. cmd:: String Notation @qualid @qualid__parse @qualid__print : @scope_name
    :name: String Notation