From 0336e86ea5ef63a587aae695adeeb4607346c337 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 31 Oct 2018 20:32:11 +0100
Subject: Giving to type_scope a softer role in printing.

Namely, it does not explicitly open a scope, but we remember that we
don't need the %type delimiter when in type position.
---
 doc/sphinx/user-extensions/syntax-extensions.rst | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx')

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
-- 
cgit v1.2.3