Interactions

There are 3 view parts in the interface:

the editor, which is used to view a Coq file. It has syntax highlighting, and when a part is evaluated, the part cannot be edited anymore (as in most interactive theorem prover editors).
the top-level, use to show the result of the interactions.
the outline not shown for every prover, which able to view a summary of the currently edited files.

All the interactions are done through the usse of a toolbar.

From left to right, the meanings of the buttons:

the first one launch or reset Prover Editor on the currently read file.
the second is used to progress through a proof (Ctrl+Alt+Down Arrow)
the third is made to undo a step in a proof (Ctrl+Alt+Up Arrow)
the fourth is made to try to progress until the end of the currently edited file
the fifth is bound to go back to the beginning of a file
the sixth one, is to cancel the current interaction with the prover. This last button is to use with the first button, as it is useful to restart everything if we are in an inconsistent state of the editor (it should not happen really often, but it is useful to be able to reset the editor state).

Some of these commands are binded to some keyboard shortcuts as detailed in the next section.