elaborator-reflection.rst: Fix rendering of bulleted list
reST requires a blank line before a bulleted list, otherwise it just renders
the whole mess as a paragraph with a lot of dashes in it.
commit002e9b9f89ed9c43be99a4bb554e5038a8933d20
authorJeremy W. Sherman <jeremyw.sherman@gmail.com>
dateSat 10 Oct 2015, 16:54 (11 years ago)
parent2cda43e
docs/reference/elaborator-reflection.rst+1
@@ -79,6 +79,7 @@ It takes the name of a hole as an argument.
7979To list all available holes, use the command ``:m``.
8080
8181In interactive elaboration shell, the following commands are available:
82+
8283- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).
8384- ``:abandon`` - Same as :q
8485- ``:state`` - Displays the current state of the term being constructed.