From 849bf3600fe11fea876c9aeea69fe806b0c8c5d8 Mon Sep 17 00:00:00 2001
From: Paul Steckler <steck@stecksoft.com>
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/output')

diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 2ccca829d..b9985a594 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


From 5ddad92dfc81b0333990dc1956544e924a14600a Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Fri, 10 Mar 2017 12:00:35 -0500
Subject: Add tests for handling of warnings

---
 test-suite/output/RecognizePluginWarning.out | 0
 test-suite/output/RecognizePluginWarning.v   | 5 +++++
 test-suite/output/UsePluginWarning.out       | 1 +
 test-suite/output/UsePluginWarning.v         | 7 +++++++
 4 files changed, 13 insertions(+)
 create mode 100644 test-suite/output/RecognizePluginWarning.out
 create mode 100644 test-suite/output/RecognizePluginWarning.v
 create mode 100644 test-suite/output/UsePluginWarning.out
 create mode 100644 test-suite/output/UsePluginWarning.v

(limited to 'test-suite/output')

diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out
new file mode 100644
index 000000000..e69de29bb
diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v
new file mode 100644
index 000000000..cd667bbd0
--- /dev/null
+++ b/test-suite/output/RecognizePluginWarning.v
@@ -0,0 +1,5 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *)
+
+(* Test that mentioning a warning defined in plugins works. The failure
+mode here is that these result in a warning about unknown warnings, since the
+plugins are not known at command line parsing time. *)
diff --git a/test-suite/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out
new file mode 100644
index 000000000..47409f3ec
--- /dev/null
+++ b/test-suite/output/UsePluginWarning.out
@@ -0,0 +1 @@
+type foo = __
diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v
new file mode 100644
index 000000000..c6e005464
--- /dev/null
+++ b/test-suite/output/UsePluginWarning.v
@@ -0,0 +1,7 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *)
+
+Require Extraction.
+Axiom foo : Prop.
+
+Extraction foo.
+
-- 
cgit v1.2.3