2 files changed, 14 insertions, 0 deletions
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.