---
name: "coqtop"
section: "1"
platform: "linux"
package: "rocq"
version: "9.3.0-1"
release: "Arch Linux 2026-11-01"
platforms: ["linux"]
url: "https://new.carta.tech/coqtop"
---

# coqtop(1)

toplevel Coq system

## NAME

coqtop - toplevel Coq system

## SYNOPSIS

**coqtop** \[ options \]

## DESCRIPTION

**coqtop** is the toplevel system of Coq, for interactive use. It reads phrases on the standard input, and prints results on the standard output. For batch-oriented use of Coq, see [**coqc**(1)](/coqc/1.md).

## OPTIONS

- **-h**, **--help**

  Help. Will give you the complete list of options accepted by coqtop.

- **-I** *dir,* **--include** *dir*

  Add directory *dir* in the include path.

- **-R** *dir coqdir*

  Recursively map physical *dir* to logical *coqdir.*

- **-top** *coqdir*

  Set the toplevel name to be *coqdir* instead of Top.

- **-nois**

  Start with an empty initial state.

- **-load-ml-source** *filename*

  Load ML file *filename.*

- **-load-ml-object** *filename*

  Load ML object file *filenname.*

- **-load-vernac-source** *filename,* **-l** *filename*

  Load Coq file *filename.v.* (Load filename.)

- **-load-vernac-source-verbose** *filename,* **-lv** *filename*

  Load verbosely Coq file *filename.v.* (Load Verbose filename.)

- **-require** *lib*

  Load Coq library *lib.* (Require lib.)

- **-require-import** *lib,* **-ri** *lib*

  Load Coq library *lib* and import it. (Require Import lib.)

- **-require-export** *lib,* **-re** *lib*

  Load Coq library *lib* and transitively import it. (Require Export lib.)

- **-require-from** *root lib,* **-rfrom** *root lib*

  Load Coq library *lib.* (From root Require lib.)

- **-require-import-from** *root lib,* **-rifrom** *root lib*

  Load Coq library *lib* and import it. (From root Require Import lib.)

- **-require-export-from** *root lib,* **-refrom** *root lib*

  Load Coq library *lib* and transitively import it. (From root Require Export lib.)

- **-load-vernac-object** *lib*

  Obsolete synonym of **-require**.

- **-where**

  Print Coq's standard library location and exit.

- **-v**

  Print Coq version and exit.

- **-q**

  Skip loading of rcfile (resource file) if any.

- **-init-file** *filename*

  Set the rcfile to *filename.*

- **-batch**

  Batch mode (exits just after arguments parsing).

- **-emacs**

  Tells Coq it is executed under Emacs.

- **-dump-glob** *filename*

  Dump globalizations in file *filename* (to be used by [**coqdoc**(1)](/coqdoc/1.md)).

- **-impredicative-set**

  Set sort Set impredicative.

- **-dont-load-proofs**

  Don't load opaque proofs in memory.

## SEE ALSO

[**coqc**(1)](/coqc/1.md), [**coq-tex**(1)](/coq-tex/1.md), [**coqdep**(1)](/coqdep/1.md)

*The Rocq Prover Reference Manual.*

The Rocq Prover website: https://rocq-prover.org