When you start CtCoq two windows appear on the screen. Each of these window is equipped with a "File" pulldown menu where you can also find an option to terminate the system. The two windows have the following aspect:

  1. A "Centaur messages" window, with the following aspect:

    This window will display all the error messages, whether they come from a misuse of CtCoq or from a misuse of Coq. However, it may happen that the Coq messages are incomplete, due to errors in the communication protocol between the two processes. To work around this problem, see the page on extra tools. The File menu of this messages window is quite important. It contains options that will come handy when you want to change resources in the middle of a session.
  2. A main CtCoq window with the following aspect:

    This window contains a lot of active areas that are described in other sections.

    1. The menu bar. This window provides a variety of pull down menus to act on the data in the Commands window.
    2. The Commands window. This window will contain the sequence of all the commands you send to the proof engine.
    3. The Tool bar This window provides a handfull of tools for quick interaction with the proof engine.
    4. The State window. This window contains the current set of goals when you perform goal direct proofs. It is also used for proof-by-pointing and drag and drop rewrite.
    5. The Theorems window. This window contains the results of Check and Search queries. It is also used for proof-by-pointing.
    3. The grey lines between each area can be used to change the respective side of each window. These windows are not equipped with horizontal scrollbars, but you can make them scroll by clicking with the left button inside the window and dragging the mouse outside the window. As soon as the mouse crosses the border, this provokes a scrolling of the window content.
  3. Auxiliary CtCoq windows can be obtained when selecting the "New Proof Window" option in the File menu of the main CtCoq window. Auxiliary CtCoq windows have basically the same look as the main window, but they have a few extra features: they are equipped with a kill box, a small square displayed at the extreme left of the menu bar, this kill box makes it possible to remove these windows from the screen without terminating the system. They also provide more options in the File menu, that make it possible to move data from one CtCoq window to another will respecting the coherence of the script. To know more about this, please refer to the page on script management. Auxiliary CtCoq windows have been introduced to make it easier to prove extra lemmas on the side when attempting a large proof.
  4. Proof text windows can be obtained when you request to display the text of a proof.

    These windows are organized to make it easy to browse through proofs containing several theorems, with a cache to ensure quick interaction. All this behavior is described in the page on textual explanation.
  5. Library windows are created when you want to keep the contents of the Theorems window on the side, in a more permanent place than the Theorems window.

    They can be used to organize little menus of commonly used theorems, as described in another page. This is especially useful as these windows can also be used for proof by pointing.
  6. Goal windows make it possible to visualize a single goal in a separate window.

    These windows are created when you go back in history and request to see the goal on which a past command worked. It should also be used to see the current goals one by one, but this is not done in the current version.