From c609c05cf4a5a2a36ca46a0ea890c954d0ae2a5b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 12 Nov 2020 20:21:36 +0100
Subject: [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.
---
 doc/sphinx/language/extensions/canonical.rst | 31 +++++++++++++---------------
 1 file changed, 14 insertions(+), 17 deletions(-)

(limited to 'doc/sphinx/language/extensions')

diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index 48120503af..ec3e3e8aa6 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -87,29 +87,26 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       If a same field occurs in several canonical structures, then
       only the structure declared first as canonical is considered.
 
-   .. attr:: canonical(false)
-
-      To prevent a field from being involved in the inference of
-      canonical instances, its declaration can be annotated with the
-      :attr:`canonical(false)` attribute (cf. the syntax of
-      :n:`@record_field`).
+.. attr:: canonical
 
-      .. example::
+   This boolean attribute can decorate a :cmd:`Definition` or
+   :cmd:`Let` command.  It is equivalent to having a :cmd:`Canonical
+   Structure` declaration just after the command.
 
-         For instance, when declaring the :g:`Setoid` structure above, the
-         :g:`Prf_equiv` field declaration could be written as follows.
+   To prevent a field from being involved in the inference of
+   canonical instances, its declaration can be annotated with
+   ``canonical=no`` (cf. the syntax of :n:`@record_field`).
 
-         .. coqdoc::
+   .. example::
 
-            #[canonical(false)] Prf_equiv : equivalence Carrier Equal
+      For instance, when declaring the :g:`Setoid` structure above, the
+      :g:`Prf_equiv` field declaration could be written as follows.
 
-      See :ref:`canonicalstructures` for a more realistic example.
+      .. coqdoc::
 
-.. attr:: canonical
+         #[canonical=no] Prf_equiv : equivalence Carrier Equal
 
-   This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command.
-   It is equivalent to having a :cmd:`Canonical Structure` declaration just
-   after the command.
+   See :ref:`canonicalstructures` for a more realistic example.
 
 .. cmd:: Print Canonical Projections {* @reference }
 
@@ -331,7 +328,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``.
                         LE_class : LE.class T;
                         extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
 
-    Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }.
+    Structure type := _Pack { obj : Type; #[canonical=no] class_of : class obj }.
 
     Arguments Mixin {e le} _.
 
-- 
cgit v1.2.3


From ca42305f1ed1699065cffdef7d96bf5fcc0069be Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 14 Nov 2020 18:44:57 +0100
Subject: Review commit: improving the doc of boolean attributes.

---
 doc/sphinx/language/extensions/canonical.rst | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/language/extensions')

diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index ec3e3e8aa6..f7ce7f1c6c 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -87,7 +87,8 @@ in :ref:`canonicalstructures`; here only a simple example is given.
       If a same field occurs in several canonical structures, then
       only the structure declared first as canonical is considered.
 
-.. attr:: canonical
+.. attr:: canonical{? = {| yes | no } }
+   :name: canonical
 
    This boolean attribute can decorate a :cmd:`Definition` or
    :cmd:`Let` command.  It is equivalent to having a :cmd:`Canonical
@@ -106,7 +107,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          #[canonical=no] Prf_equiv : equivalence Carrier Equal
 
-   See :ref:`canonicalstructures` for a more realistic example.
+   See :ref:`hierarchy_of_structures` for a more realistic example.
 
 .. cmd:: Print Canonical Projections {* @reference }
 
@@ -245,6 +246,8 @@ for each component of the pair. The declaration associates to the key ``*``
 relation ``pair_eq`` whenever the type constructor ``*`` is applied to two
 types being themselves in the ``EQ`` class.
 
+.. _hierarchy_of_structures:
+
 Hierarchy of structures
 ----------------------------
 
-- 
cgit v1.2.3