From 9bc339f529fc2ee2389a717914514829a73686bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Sep 2018 23:14:29 +0200
Subject: Fixing #8551 (missing delimiters when notation exists both lonely and
 in scope).

---
 test-suite/output/Notations4.out |  2 ++
 test-suite/output/Notations4.v   | 12 ++++++++++++
 2 files changed, 14 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index d25ad5dca8..acd69f3f50 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -21,3 +21,5 @@ Let "x" e1 e2
      : expr
 Let "x" e1 e2
      : expr
+fun x : nat => (# x)%nat
+     : nat -> nat
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 191a073051..12e98c3d64 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -94,3 +94,15 @@ Coercion App : expr >-> Funclass.
 Check (Let "x" e1 e2).
 
 End D.
+
+(* Check fix of #8551: a delimiter should be inserted because the
+   lonely notation hides the scope nat_scope, even though the latter
+   is open *)
+
+Module E.
+
+Notation "# x" := (S x) (at level 20) : nat_scope.
+Notation "# x" := (Some x).
+Check fun x => (# x)%nat.
+
+End E.
-- 
cgit v1.2.3