1COQ(1)                      General Commands Manual                     COQ(1)
2
3
4

NAME

6       coqc - The Coq Proof Assistant compiler
7
8
9

SYNOPSIS

11       coqc [ general  Coq  options ] file
12
13
14

DESCRIPTION

16       coqc  is  the  batch compiler for the Coq Proof Assistant.  The options
17       are basically the same as coqtop(1).  file.v is the vernacular file  to
18       compile.   file  must  be  formed only with the characters `a` to  `Z`,
19       `0`-`9` or `_` and must begin with a letter.  The compiler produces  an
20       object file file.vo.
21
22       For interactive use of Coq, see coqtop(1).
23
24
25

OPTIONS

27       coqc  is  a  script  that  simply  runs  coqtop with option -compile it
28       accepts the same options as coqtop.
29
30
31       -image bin
32              use bin as underlying coqtop instead of the default one.
33
34
35       -verbose
36              print the compiled file on the standard output.
37
38

SEE ALSO

40       coqtop(1), coq_makefile(1), coqdep(1).
41       The Coq Reference Manual.  The Coq web site: http://coq.inria.fr
42
43
44
45                                April 25, 2001                          COQ(1)