From 8b490bcab7b52727222818db3634575f0fef8eff Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Wed, 15 May 2024 11:02:11 +0200 Subject: [PATCH] additions/corrections about scopes in the refman --- doc/sphinx/user-extensions/syntax-extensions.rst | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) 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,