diff options
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/02-specification-language/13312-attributes+bool_single.rst | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst new file mode 100644 index 0000000000..f069bc616b --- /dev/null +++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst @@ -0,0 +1,17 @@ +- **Changed:** + :term:`Boolean attributes <boolean attribute>` are now specified using + key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`. + If the value is missing, the default is :n:`yes`. The old syntax is still + supported, but produces the ``deprecated-attribute-syntax`` warning. + + Deprecated attributes are :attr:`universes(monomorphic)`, + :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are + respectively replaced by :attr:`universes(polymorphic=no) <universes(polymorphic)>`, + :attr:`universes(template=no) <universes(template)>` + and :attr:`universes(cumulative=no) <universes(cumulative)>`. + Attributes :attr:`program` and :attr:`canonical` are also affected, + with the syntax :n:`@ident__attr(false)` being deprecated in favor of + :n:`@ident__attr=no`. + + (`#13312 <https://github.com/coq/coq/pull/13312>`_, + by Emilio Jesus Gallego Arias). |