Merge PR#813: Fix plugin warnings

4 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/RecognizePluginWarning.out
diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v
new file mode 100644
index 0000000000..cd667bbd00
--- /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 0000000000..47409f3ec5
--- /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 0000000000..c6e0054641
--- /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.
+