coqc1
Coq compiler
Usage
coqc [general
Coq
options]
file
Overview
coqc is the batch compiler for the Coq Proof Assistant. The options are basically the same as coqtop(1). file.v is the vernacular file to compile. file must be formed only with the characters `a' to `Z', `0' to `9' or `_' and must begin with a letter. The compiler produces an object file file.vo.
For interactive use of Coq, see coqtop(1).
Options
coqc is a script that simply runs coqtop with option -compile. It accepts the same options as coqtop.
-imagebin-
Use bin as underlying
coqtopinstead of the default one.
-
-verbose -
Print the compiled file on the standard output.
Releases
14 releases since Debian 2.2 (Potato); the text changed 6 times.
-verbose since Debian 8 (Jessie).
-batch until Debian 2.2 (Potato);
-h until Debian 4.0 (Etch);
-i until Debian 2.2 (Potato).