5.8 Miscellaneous
5.8.1 Quit.
This command permits to quit Coq.5.8.2 Drop.
This command permits to leave Coq temporarily and enter the Objective Caml toplevel. The Objective Caml commands#use "include.ml";; go();;
will allow subsequently to return to Coq's toplevel in the same state. This is used mostly as a debug facility by Coq'implementors and does not concern the casual user.
Warning: 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).
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).