From 6bff5ed8ef6ef6148e035f80e26e60d050e79c43 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 10 Dec 2019 23:10:26 +0100
Subject: Fixing #10750 (anomaly of "Print Visibility" on only-printing
 notations).

---
 test-suite/success/Notations2.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index d047f7560e..aa439fae12 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -165,3 +165,10 @@ Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pa
 Check fun y : nat => # (x,z) ## y & y.
 
 End M17.
+
+Module Bug10750.
+
+Notation "#" := 0 (only printing).
+Print Visibility.
+
+End Bug10750.
-- 
cgit v1.2.3