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

NAME

6       coqnative - The Coq native compiler
7
8
9

SYNOPSIS

11       coqnative [ options ] filename
12
13
14

DESCRIPTION

16       coqnative  compiles vo files to binary files used by the native compute
17       mechanism of the Coq Proof Assistant. See the Reference Manual for more
18       information.  It  returns  with  exit code 0 if all the requested tasks
19       succeeded. A non-zero return code means that something went wrong.
20
21       filename is a Coq object file (a .vo) to compile to a native binary.
22
23

OPTIONS

25       -Q dir coqdir
26              map physical dir to logical coqdir
27
28
29       -R dir coqdir
30              synonymous for -Q
31
32
33       -I dir ignored, for compatibility
34
35
36       -noinit
37              ignored, for compatibility
38
39
40       -boot  boot mode
41
42
43       -coqlib dir
44              override the default location of the standard library
45
46
47       -nI dir
48              add dir to the set of paths for the native files of  the  depen‐
49              dencies
50
51
52       -native-output-dir dir
53              output the generated files to dir
54
55
56       -h, --help
57              print list of options
58
59

SEE ALSO

61       coqtop(1), coqc(1), coq_makefile(1), coqdep(1).
62       The Coq Reference Manual.  The Coq web site: http://coq.inria.fr
63
64
65
66                                                                        COQ(1)
Impressum