Rocq < Toplevel input, characters 17-29:
> #[canonical=yes, canonical=no] Definition a := 3.
> ^^^^^^^^^^^^
Error: Attribute for canonical specified twice.
Rocq < Rocq < Toplevel input, characters 29-43:
> #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3.
> ^^^^^^^^^^^^^^
Error: key 'polymorphic' has been already set.
Rocq < Rocq < Toplevel input, characters 13-28:
> #[universes(polymorphic=foo)] Definition a := 3.
> ^^^^^^^^^^^^^^^
Error: Invalid value 'foo' for key polymorphic
use one of {yes, no}
Rocq < Rocq < Toplevel input, characters 13-29:
> #[universes(polymorphic(foo))] Definition a := 3.
> ^^^^^^^^^^^^^^^^
Error: Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead.
Rocq < Rocq < Toplevel input, characters 13-33:
> #[universes(polymorphic(foo,bar))] Definition a := 3.
> ^^^^^^^^^^^^^^^^^^^^
Error: Invalid syntax polymorphic(foo, bar), try polymorphic={yes,
no} instead.
Rocq < Rocq < Toplevel input, characters 30-37:
> #[universes(polymorphic=yes, bla=bla)] Definition a := 3.
> ^^^^^^^
Error: This command does not support this attribute: universes.
[unsupported-attributes,parsing,default]
Rocq <
[ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
]
