6.3 Displaying information

6.3.1 Show.

1. Show num.
   Displays only the num-th subgoal.
   
   Error message: no such goal
   
   
2. Show Implicits.
   Displays the current goals, printing the implicit arguments of constants.
   
   
3. Show Implicits num.
   Same as above, only displaying the num-th subgoal.
   
   
4. Show Script.
   Displays the whole list of tactics applied from the beginning of the current proof. This tactics script may contain some holes (subgoals not yet proved). They are printed as <Your Tactic Text here>.
   
   
5. Show Tree.
   This command can be seen as a more structured way of displaying the state of the proof than that provided by Show Script. Instead of just giving the list of tactics that have been applied, it shows the derivation tree constructed by then. Each node of the tree contains the conclusion of the corresponding sub-derivation (i.e. a goal with its corresponding local context) and the tactic that has generated all the sub-derivations. The leaves of this tree are the goals which still remain to be proved.
   
   
6. Show Proof.
   It displays the proof term generated by the tactics that have been applied. If the proof is not completed, this term contain holes, which correspond to the sub-terms which are still to be constructed. These holes appear as a question mark indexed by an integer, and applied to the list of variables in the context, since it may depend on them. The types obtained by abstracting away the context from the type of each hole-placer are also printed.
   
   
7. Show Conjectures.
   It prints the list of the names of all the theorems that are currently being proved. As it is possible to start proving a previous lemma during the proof of a theorem, this list may contain several names.

6.3.2 Set Hyps_limit num.

6.3.3 Unset Hyps_limit.