Linux Certif

Toute la documentation sur la certification Linux LPI

coqmktop

NAME

coqmktop - The Coq Proof Assistant user-tactics linker

SYNOPSIS

coqmktop [ options ] files

DESCRIPTION

coqmktop builds a new Coq toplevel extended with user-tactics. files are the Objective Caml object or library files (i.e. with suffix .cmo, The linker produces an executable Coq toplevel which can be called directly or through coqc(1), using the -image option.

OPTIONS

-h

Help. List the available options.

-srcdir dir

Specify where the Coq source files are

-o exec-file

Specify the name of the resulting toplevel

-opt

Compile in native code

-full

Link high level tactics

-top

Build Coq on a ocaml toplevel (incompatible with -opt)

-searchisos

Build a toplevel for SearchIsos

-ide

Build a toplevel for the Coq IDE

-R dir

Specify recursively directories for Ocaml

-v8

Link with V8 grammar

SEE ALSO

coqtop(1), ocamlmktop(1). ocamlc(1). ocamlopt(1).
The Coq Reference Manual. The Coq web site: http://coq.inria.fr