Rechercher une page de manuel
coqmktop
Langue: en
Version: 110798 (mandriva - 01/05/08)
Section: 1 (Commandes utilisateur)
NAME
coqmktop - The Coq Proof Assistant user-tactics linkerSYNOPSIS
coqmktop [ options ] filesDESCRIPTION
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
Contenus ©2006-2024 Benjamin Poulain
Design ©2006-2024 Maxime Vantorre