diff options
| author | Emilio Jesus Gallego Arias | 2020-11-16 16:18:06 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-18 16:25:00 +0100 |
| commit | efa6673158f5eaa3fc11c0b3d1e3285c4acc129a (patch) | |
| tree | 79d8b3cccd9759fc63cf22998e191928870e6993 /test-suite | |
| parent | 6aeee2e4e37d4b8ffb8c50c109903ad336c8bdfa (diff) | |
[attributes] Add output test suite for errors, improve error printing.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/attributes.out | 11 | ||||
| -rw-r--r-- | test-suite/output/attributes.v | 9 |
2 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/output/attributes.out b/test-suite/output/attributes.out new file mode 100644 index 0000000000..25572ee2aa --- /dev/null +++ b/test-suite/output/attributes.out @@ -0,0 +1,11 @@ +The command has indeed failed with message: +Attribute for canonical specified twice. +The command has indeed failed with message: +key 'polymorphic' has been already set. +The command has indeed failed with message: +Invalid value 'foo' for key polymorphic +use one of {yes, no} +The command has indeed failed with message: +Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead. +The command has indeed failed with message: +Invalid syntax polymorphic(foo, bar), try polymorphic={yes, no} instead. diff --git a/test-suite/output/attributes.v b/test-suite/output/attributes.v new file mode 100644 index 0000000000..aef05e6cd4 --- /dev/null +++ b/test-suite/output/attributes.v @@ -0,0 +1,9 @@ +Fail #[canonical=yes, canonical=no] Definition a := 3. + +Fail #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3. + +Fail #[universes(polymorphic=foo)] Definition a := 3. + +Fail #[universes(polymorphic(foo))] Definition a := 3. + +Fail #[universes(polymorphic(foo,bar))] Definition a := 3. |