From 849bf3600fe11fea876c9aeea69fe806b0c8c5d8 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Fri, 9 Jun 2017 12:30:42 -0400
Subject: Fix Bug #5568, no dup notation warnings on repeated module imports

---
 test-suite/output/Notations.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 2ccca829d6..b9985a594f 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -1,3 +1,14 @@
+(* Bug 5568, don't warn for notations in repeated module import *)
+
+Module foo.
+Notation compose := (fun g f => g f).
+Notation "g & f" := (compose g f) (at level 10).
+End foo.
+
+Import foo.
+Import foo.
+Import foo.
+
 (**********************************************************************)
 (* Notations for if and let (submitted by Roland Zumkeller)           *)
 
-- 
cgit v1.2.3