diff options
| author | Clément Pit-Claudel | 2018-07-30 15:14:53 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-07-30 15:16:25 -0400 |
| commit | 7f1ed3298c841c2afa4faf080a5f65361bbb413f (patch) | |
| tree | b3917392b1b07818f07bb7d9b39cdc628b3e539e /doc/sphinx/proof-engine/proof-handling.rst | |
| parent | 1b2decc1bc0db2a58fcc4a4e6e572aed645bab29 (diff) | |
[sphinx] Use arguments of '.. example::' directive as a title
Most existing uses of .. example did not use the first line as a title, so this
commit also adds appropriate blank lines.
Diffstat (limited to 'doc/sphinx/proof-engine/proof-handling.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 44376080c3..a9d0c16376 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -375,6 +375,7 @@ or focus the next one. The following example script illustrates all these features: .. example:: + .. coqtop:: all Goal (((True /\ True) /\ True) /\ True) /\ True. @@ -511,6 +512,7 @@ Requesting information :token:`ident` .. example:: + .. coqtop:: all Show Match nat. |