diff options
| author | Théo Zimmermann | 2019-02-26 16:33:08 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-28 14:26:41 +0100 |
| commit | 9c201fe42142de7332149863d6c1343c2dec8391 (patch) | |
| tree | c97b2599ade286f79c88d07f335f215112fc0018 /doc/sphinx/addendum | |
| parent | 9d6f268723b6352a97bcc3baf0df57f1c1b251fa (diff) | |
[sphinx] Add warn option to coqtop directive.
By default Coq warnings are made fatal when building the manual.
If you want to show a command resulting in a warning, use the warn
option.
Preexisting warnings are either fixed or marked as expected.
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 8 |
1 files changed, 6 insertions, 2 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. |