Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
COQ(1)			    General Commands Manual			COQ(1)

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,
       .cmx,  .cma or .cmxa) to	link with the Coq system.  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)

       -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

				April 25, 2001				COQ(1)

NAME | SYNOPSIS | DESCRIPTION | OPTIONS | SEE ALSO

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=coqmktop&sektion=1&manpath=FreeBSD+12.1-RELEASE+and+Ports>

home | help