diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index d291d6e1b6245..6ec7da0f461b9 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1485,8 +1485,10 @@ Most commands use :token:`scope_name`; :token:`scope_key`\s are used within :tok
 
    Declares a new notation scope. Note that the initial
    state of Coq declares the following notation scopes:
-   ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``,
-   ``bool_scope``, ``list_scope``, ``dec_int_scope``, ``dec_uint_scope``.
+
+   ``bool_scope``, ``byte_scope``, ``core_scope``, ``dec_int_scope``,
+   ``dec_uint_scope``, ``function_scope``, ``hex_int_scope``, ``hex_nat_scope``,
+   ``hex_uint_scope``, ``list_scope``, ``nat_scope``, ``type_scope``.
 
    Use commands such as :cmd:`Notation` to add notations to the scope.
 
@@ -1510,6 +1512,10 @@ stack, rather than through "pop" operations.
 
 Use the :cmd:`Print Visibility` command to display the current notation scope stack.
 
+The initial state of coq has the following scopes opened: ``core_scope``,
+``function_scope``, ``type_scope`` and ``nat_scope``, ``nat_scope`` being the
+top of the scopes stack.
+
 .. cmd:: Open Scope @scope
 
    Adds a scope to the notation scope stack.  If the scope is already present,