@@ -79,6 +79,7 @@ It takes the name of a hole as an argument.
79To list all available holes, use the command ``:m``.
79To list all available holes, use the command ``:m``.
81In interactive elaboration shell, the following commands are available:
81In interactive elaboration shell, the following commands are available:
82- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).
83- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).
83- ``:abandon`` - Same as :q
84- ``:abandon`` - Same as :q
84- ``:state`` - Displays the current state of the term being constructed.
85- ``:state`` - Displays the current state of the term being constructed.