@@ -74,18 +74,25 @@ We can generate identity functions at any concrete type using the same script:
7474Interactively Building Elab Scripts
7575===================================
7676
77−To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.
78−It takes the name of a hole as an argument.
79−To list all available holes, use the command ``:m``.
80−
81−In interactive elaboration shell, the following commands are available:
82−
83−- ``:q`` - Quits the elaboration shell (gives up on proving current lemma).
84−- ``:abandon`` - Same as :q
85−- ``:state`` - Displays the current state of the term being constructed.
86−- ``:term`` - Displays the current proof term complete with its yet-to-be-filled holes.
87−- ``:undo`` - Undoes the last tactic.
88−- ``:qed`` - Once the elaboration shell tells you "No more goals," you get to type this in celebration! (Completes the construction and exits the shell)
77+You can build an ``Elab`` script interactively at the REPL.
78+Use the command ``:metavars``, or ``:m`` for short, to list the available holes.
79+Then, issue the ``:elab <hole>`` command at the REPL
80+to enter the elaboration shell.
81+
82+The interactive elaboration shell accepts the following commands:
83+
84+- ``:abandon``, or ``:q`` for short,
85+ quits the elaboration shell, which abandons proving the current lemma.
86+
87+- ``:state`` displays the current state of the term being constructed.
88+
89+- ``:term`` displays the current proof term as well as its yet-to-be-filled holes.
90+
91+- ``:undo`` undoes the last tactic.
92+
93+- ``:qed`` finishes the script and exits the elaboration shell. The shell will only accept
94+ this command once it reports, "No more goals." On exit, it will print out the finished
95+ elaboration script for you to copy into your program.
8996
9097
9198Failure