Man page or keyword search:   man All Sections 1 - General Commands 2 - System Calls 3 - Subroutines, Functions 4 - Special Files 5 - File Formats 6 - Games and Screensavers 7 - Macros and Conventions 8 - Maintenence Commands 9 - Kernel Interface New Commands Server 4.4BSD AIX Alpinelinux Archlinux Aros BSDOS BSDi Bifrost CentOS Cygwin Darwin Debian DigitalUNIX DragonFly ElementaryOS Fedora FreeBSD Gentoo GhostBSD HP-UX Haiku Hurd IRIX Inferno JazzOS Kali Knoppix LinuxMint MacOSX Mageia Mandriva Manjaro Minix MirBSD NeXTSTEP NetBSD OPENSTEP OSF1 OpenBSD OpenDarwin OpenIndiana OpenMandriva OpenServer OpenSuSE OpenVMS Oracle PC-BSD Peanut Pidora Plan9 QNX Raspbian RedHat Scientific Slackware SmartOS Solaris SuSE SunOS Syllable Tru64 UNIXv7 Ubuntu Ultrix UnixWare Xenix YellowDog aLinux   44335 pages apropos Keyword Search (all sections) Output format html ascii pdf view pdf save postscript

COQ(1)									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)

Vote for polarhome