[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.

We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).

We update the documentation, test-suite, and changelog.

1 files changed, 13 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..fa046d968f
--- /dev/null
+++ b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst
@@ -0,0 +1,13 @@
+- **Changed:**
+  Boolean attributes are now specified using key/value pairs, that is
+  to say ``attr={yes,no}``. If the value is missing, the default is
+  ``on``.  Old syntax is still supported, but produces the
+  ``deprecated-attribute-syntax`` warning.
+  Attributes deprecated are ``universes(monomorphic)``,
+  ``universes(notemplate)``, ``universes(noncumulative)``, which are
+  replaced by the corresponding ``universes(polymorphic=no)`` etc...
+  Attributes :attr:`program` and :attr:`canonical` are also affected,
+  with the syntax ``attr(false)`` being deprecated in favor of
+  ``attr=no``.
+  (`#13312 <https://github.com/coq/coq/pull/13312>`_,
+  by Emilio Jesus Gallego Arias).