Add documentation

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 <https://github.com/coq/coq/pull/6134>`_,
+  fixes `#14959 <https://github.com/coq/coq/issues/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).

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 <LocalInterpretationRulesForNotations>` to
+:n:`@type` then :n:`@term10` is interpreted in that scope.
+
 .. _gallina-definitions:
 
 Top-level definitions

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 <type-cast>` :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