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.

2 files changed, 40 insertions, 0 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 40d875e8ab..d58e4bf2d6 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -33,3 +33,15 @@ fun x : nat => ## x
      : nat -> nat
 fun x : nat => (x.-1)%pred
      : nat -> nat
+∀ a : nat, a = 0
+     : Prop
+((∀ a : nat, a = 0) -> True)%type
+     : Prop
+#
+     : Prop
+# -> True
+     : Prop
+((∀ a : nat, a = 0) -> True)%type
+     : Prop
+##
+     : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4196c7e6b4..61206b6dd0 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -136,3 +136,31 @@ Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope.
 Check fun x => pred x.
 
 End G.
+
+(* Checking arbitration between in the presence of a notation in type scope *)
+
+Module H.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+Check forall a, a = 0.
+
+Close Scope type_scope.
+Check ((forall a, a = 0) -> True)%type.
+Open Scope type_scope.
+
+Notation "#" := (forall a, a = 0).
+Check #.
+Check # -> True.
+
+Close Scope type_scope.
+Check (# -> True)%type.
+Open Scope type_scope.
+
+Declare Scope my_scope.
+Notation "##" := (forall a, a = 0) : my_scope.
+Open Scope my_scope.
+Check ##.
+
+End H.