The Commands window. This window will practically contain all the commands that you send to the Coq proof assistant. A first important feature of this window is that the commands are mostly edited in a structured way, with some accelerators provided by advanced tools such as Proof-by-pointing. A second important feature is that the commands recorded in this window are managed by a script management tool, that ensures that the relevant commands are kept in an order that respects the current state of the proof engine.

Actions can be performed on this window using the options of the menus that appear in the menubar on top of the window. Other actions can be performed using keyboard accelerators.

The contents of this window can be saved as plain Coq input, in postscript format, or in polish format.