diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 2 |
2 files changed, 7 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 3e414a714c..a9d894cab5 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -313,7 +313,9 @@ 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. -.. coqtop:: all +.. FIXME shouldn't warn + +.. coqtop:: all warn Module Add_instance_attempt. @@ -418,7 +420,9 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. coqtop:: all +.. FIXME should not warn + +.. coqtop:: all warn Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 3ec6c118af..e882ce6e88 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -285,7 +285,7 @@ By default, implicit arguments are omitted in patterns. So we write: .. coqtop:: all - Arguments nil [A]. + Arguments nil {A}. Arguments cons [A] _ _. Check (fun l:List nat => |