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.
---
 test-suite/output/Notations4.out | 12 ++++++++++++
 test-suite/output/Notations4.v   | 28 ++++++++++++++++++++++++++++
 2 files changed, 40 insertions(+)

(limited to 'test-suite')

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