---
name: "coqmktop"
section: "1"
platform: "linux"
package: "libcoq-ocaml-dev"
version: "8.6-4"
release: "Debian 9 (Stretch)"
platforms: ["linux"]
url: "https://new.carta.tech/coqmktop"
---

# coqmktop(1)

The Coq Proof Assistant user-tactics linker

## 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)](/coqc/1.md), 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)](/coqtop/1.md), [**ocamlmktop**(1)](/ocamlmktop/1.md). [**ocamlc**(1)](/ocamlc/1.md). [**ocamlopt**(1)](/ocamlopt/1.md).\
 *The Coq Reference Manual.* *The Coq web site: http://coq.inria.fr*