11.1 Interactive use (coqtop)

In the interactive mode, also known as the Coq toplevel, the user can develop his theories and proofs step by step. The Coq toplevel is run by the command coqtop.

They are two different binary images of Coq: the byte-code one and the native-code one (if Objective Caml provides a native-code compiler for your platform, which is supposed in the following). When invoking coqtop or coqc, the native-code version of the system is used. The command-line options -byte and -opt explicitly select the byte-code and the native-code versions, respectively.

The byte-code toplevel is based on a Caml toplevel (to allow the dynamic link of tactics). You can switch to the Caml toplevel with the command Drop., and come back to the Coq toplevel with the command Toplevel.loop();;.