From 4c642b5c27d4f9c355044cb585a645b50dd844f2 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 6 May 2019 17:38:39 +0000
Subject: [User manual] Fix two warnings related to canonical structures

---
 doc/sphinx/addendum/canonical-structures.rst | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index dd21ea09bd..d81dafa4db 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -209,7 +209,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; class_of : class obj }.
+    Structure type := _Pack { obj : Type; #[not_canonical] class_of : class obj }.
 
     Arguments Mixin {e le} _.
 
@@ -219,6 +219,9 @@ The mixin component of the ``LEQ`` class contains all the extra content we
 are adding to ``EQ`` and ``LE``. In particular it contains the requirement
 that the two relations we are combining are compatible.
 
+The `class_of` projection of the `type` structure is annotated as *not canonical*;
+it plays no role in the search for instances.
+
 Unfortunately there is still an obstacle to developing the algebraic
 theory of this new class.
 
@@ -313,9 +316,7 @@ constructor ``*``. It also tests that they work as expected.
 Unfortunately, these declarations are very verbose. In the following
 subsection we show how to make them more compact.
 
-.. FIXME shouldn't warn
-
-.. coqtop:: all warn
+.. coqtop:: all
 
   Module Add_instance_attempt.
 
@@ -420,9 +421,7 @@ the reader can refer to :cite:`CSwcu`.
 
 The declaration of canonical instances can now be way more compact:
 
-.. FIXME should not warn
-
-.. coqtop:: all warn
+.. coqtop:: all
 
   Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
   
-- 
cgit v1.2.3


From 34e84eafe6615055071fbdc4aaee70c4c161a0fb Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 9 May 2019 13:39:25 +0000
Subject: [Attributes] Allow explicit value for two-valued attributes

Attributes that enable/disable a feature can have an explicit value
(default is enable when the attribute is present).

Three-valued boolean attributes do not support this:
what would `#[local(false)]` mean?
---
 doc/sphinx/addendum/canonical-structures.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/addendum')

diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index d81dafa4db..b593b0cef1 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -209,7 +209,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; #[not_canonical] class_of : class obj }.
+    Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }.
 
     Arguments Mixin {e le} _.
 
-- 
cgit v1.2.3