From 2e64c61cf64172fb0dce2d8b3996fb30e179e5ea Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Feb 2020 01:43:43 +0100
Subject: Fixing a bug introduced in PR #10832 (new format specific to a given
 notation).

The import of the format should not be done if i<>1 in open_notation.
---
 test-suite/success/Notations2.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index aa439fae12..b26e725d9b 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -172,3 +172,16 @@ Notation "#" := 0 (only printing).
 Print Visibility.
 
 End Bug10750.
+
+Module M18.
+
+  Module A.
+    Module B.
+    Infix "+++" := Nat.add (at level 70).
+    End B.
+  End A.
+Import A.
+(* Check that the notation in module B is not visible *)
+Infix "+++" := Nat.add (at level 80).
+
+End M18.
-- 
cgit v1.2.3