---
name: "ssrcoq"
section: "1"
platform: "linux"
package: "libssreflect-coq"
version: "1.3pl4-1"
release: "Debian 7 (Wheezy)"
platforms: ["linux"]
url: "https://new.carta.tech/coqtop"
---

# ssrcoq(1)

The Coq Proof Assistant toplevel system

Part of [coqtop(1)](/coqtop/1.md).

## NAME

coqtop - The Coq Proof Assistant toplevel 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

- **-inputstate** *filename,* **-is** *filename*

  read state from file *filename.coq*

- **-nois**

  start with an empty initial state

- **-outputstate***filename*

  write state in file *filename.coq*

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

  load ML object file *filenname*

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

  load ML file *filename*

- **-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.)

- **-load-vernac-object** *filename*

  load Coq object file *filename.vo*

- **-require** *filename*

  load Coq object file *filename.vo* and import it (Require Import filename.)

- **-compile** *filename*

  compile Coq file *filename.v* (implies  **-batch** )

- **-compile-verbose** *filename*

  verbosely compile Coq file *filename.v* (implies  **-batch** )

- **-opt**

  run the native-code version of Coq

- **-byte**

  run the bytecode version of Coq

- **-where**

  print Coq's standard library location and exit

- **-v**

  print Coq version and exit

- **-q**

  skip loading of rcfile

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

  set the rcfile to *filename*

- **-user** *uid*

  use the rcfile of user *uid*

- **-batch**

  batch mode (exits just after arguments parsing)

- **-boot**

  boot mode (implies **-q** and **-batch** )

- **-emacs**

  tells Coq it is executed under Emacs

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

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

- **-with-geoproof** *(yes\|no)*

  to (de)activate special functions for Geoproof within Coqide (default is *yes* )

- **-impredicative-set**

  set sort Set impredicative

- **-dont-load-proofs**

  don't load opaque proofs in memory

- **-xml**

  export XML files either to the hierarchy rooted in the directory $COQ\_XML\_LIBRARY\_ROOT (if set) or to stdout (if unset)

- **-quality**

  improve the legibility of the proof terms produced by some tactics

## SEE ALSO

[**coqc**(1)](/coqc/1.md), [**coq-tex**(1)](/coq-tex/1.md), [**coqdep**(1)](/coqdep/1.md).\
 *The Coq Reference Manual.* *The Coq web site: http://coq.inria.fr*