diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ce79e2915e..a5869055fa 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1340,7 +1340,16 @@ Coq will use the following rules for printing priorities: have a delimiter are considered, giving priority to the most recently defined (or imported) ones. The corresponding delimiter is inserted, making the corresponding scope the most recent explicitly - open scope for all subterms of the current term. + open scope for all subterms of the current term. As an exception to + the insertion of the corresponding delimiter, when an expression is + statically known to be in a position expecting a type and the + notation is from scope ``type_scope``, and the latter is closed, the + delimiter is not inserted. This is because expressions statically + known to be in a position expecting a type are by default + interpreted with `type_scope` temporarily activated. Expressions + statically known to be in a position expecting a type typically + include being on the right-hand side of `:`, `<:`, `<<:` and after + the comma in a `forall` expression. - As a refinement of the previous rule, in the case of applied global references, notations in a non-opened scope with delimiter |