5.8 Miscellaneous

5.8.1 Quit.

This command permits to quit Coq.

5.8.2 Drop.

This is used mostly as a debug facility by Coq's implementors and does not concern the casual user. This command permits to leave Coq temporarily and enter the Objective Caml toplevel. The Objective Caml command:

#use "include.ml";;

add the right loadpaths and loads some toplevel printers for all abstract types of Coq- section_path, identfifiers, terms, judgements, .... You can also use the file base_include.ml instead, that loads only the pretty-printers for section_paths and identfifiers. See section 10.7 more information on the usage of the toplevel. You can return back to Coq with the command: 

go();;


Warnings:
  1. It only works if the bytecode version of Coq was invoked. It does not work if Coq was invoked with the option -opt or -full (see X).
  2. You must have downloaded the source code of Coq (not the binary distribution), to have compiled Coq and to set the environment variable COQTOP to the right value (see 11.4)

5.8.3 Begin Silent.

This command turns off the normal displaying.

5.8.4 End Silent.

This command turns the normal display on.

5.8.5 Time.

This commands turns on the Time Search Display mode. The Time Search Display mode shows the user and system times for the SearchIsos requests.

5.8.6 Untime.

This commands turns off the Time Search Display mode (see section 5.8.5).