From 3ed759015416da61ac115549fd2c71c107d29484 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 27 Sep 2023 16:45:22 +0200 Subject: [PATCH] Add documentation --- .../03-notations/6134-master+type-scope-cast.rst | 10 ++++++++++ doc/sphinx/language/core/definitions.rst | 3 +++ doc/sphinx/user-extensions/syntax-extensions.rst | 11 +++++++++++ 3 files changed, 24 insertions(+) create mode 100644 doc/changelog/03-notations/6134-master+type-scope-cast.rst diff --git a/doc/changelog/03-notations/6134-master+type-scope-cast.rst b/doc/changelog/03-notations/6134-master+type-scope-cast.rst new file mode 100644 index 000000000000..cdf386c05ac6 --- /dev/null +++ b/doc/changelog/03-notations/6134-master+type-scope-cast.rst @@ -0,0 +1,10 @@ +- **Changed:** + In casts like :g:`term : t` where :g:`t` is bound to some + scope :g:`t_scope`, via :cmd:`Bind Scope`, the :g:`term` is now + interpreted in scope :g:`t_scope`. In particular when :g:`t` + is :g:`Type` the :g:`term` is interpreted in :g:`type_scope` + and when :g:`t` is a product the :g:`term` is interpreted + in :g:`fun_scope` + (`#6134 `_, + fixes `#14959 `_, + by Hugo Herbelin, reviewed by Maxime Dénès, Jim Fehrle, Emilio Gallego, Gaëtan Gilbert, Jason Gross, Pierre-Marie Pédrot, Pierre Roux, Bas Spitters and Théo Zimmermann). diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index a2c36af41223..89638ae45b07 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -57,6 +57,9 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`) :n:`@type` without leaving a trace in the produced value. This is a :gdef:`volatile cast`. +If a scope is :ref:`bound ` to +:n:`@type` then :n:`@term10` is interpreted in that scope. + .. _gallina-definitions: Top-level definitions diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index c14b4c61c7c4..302b04aa410d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1590,6 +1590,9 @@ Binding types or coercion classes to notation scopes then :g:`a` of type :g:`t` in :g:`f t a` is not recognized as an argument to be interpreted in scope ``scope``. + In explicit :ref:`casts ` :n:`@term : @coercion_class`, the :n:`term` + is interpreted in the :token:`scope_name` associated with :n:`@coercion_class`. + This command supports the :attr:`local`, :attr:`global`, :attr:`add_top` and :attr:`add_bottom` attributes. @@ -1652,6 +1655,14 @@ Binding types or coercion classes to notation scopes About f. + Bindings are also used in casts. + + .. coqtop:: all + + Close Scope F_scope. + Check #. + Check # : bool. + .. note:: Such stacks of scopes can be handy to share notations between multiple types. For instance, the scope ``T_scope`` above could contain many generic notations used for both the