11.2 Batch compilation (coqc)
The coqc command takes a name file as argument. Then it looks for a vernacular file named file.v, and tries to compile it into a file.vo file (See 5.4). With the-i option, it compiles the specification module file.vi. Notice that the
-opt and -full options are still
available with coqc and allow you to compile Coq files with
an efficient version of the system.