diff options
| author | Théo Zimmermann | 2018-08-01 10:58:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-01 10:58:18 +0200 |
| commit | 2dcb340f82c3df70d8fe2c6acc3536913a86144a (patch) | |
| tree | 86e627cb4c13ec2b1533c557224495ed1d15908e /doc/sphinx/addendum | |
| parent | 29a432dfbaa83dd1459c7af95f556555da15a1ce (diff) | |
| parent | 7f1ed3298c841c2afa4faf080a5f65361bbb413f (diff) | |
Merge PR #8191: [sphinx] Use arguments of '.. example::' directive as a title
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index b6c35d8fa7..0f2d35d044 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -32,6 +32,7 @@ When the proof ends two constants are defined: ends with ``Qed``, and transparent if the proof ends with ``Defined``. .. example:: + .. coqtop:: all Require Coq.derive.Derive. |