diff options
| author | Tej Chajed | 2017-03-10 12:00:35 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-23 10:32:19 +0200 |
| commit | 5ddad92dfc81b0333990dc1956544e924a14600a (patch) | |
| tree | 4d37e6dc8bdf91483f15c12706864652fe0170e4 | |
| parent | 965960bcd13eb3a6e531b03fb85be516dcdca551 (diff) | |
Add tests for handling of warnings
| -rw-r--r-- | test-suite/output/RecognizePluginWarning.out | 0 | ||||
| -rw-r--r-- | test-suite/output/RecognizePluginWarning.v | 5 | ||||
| -rw-r--r-- | test-suite/output/UsePluginWarning.out | 1 | ||||
| -rw-r--r-- | test-suite/output/UsePluginWarning.v | 7 |
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. + |