GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages


Manual Reference Pages  -  COQTOP (1)

NAME

coqtop - The Coq Proof Assistant toplevel system

CONTENTS

Synopsis
Description
Options
See Also

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

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

-outputstatefilename
  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

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

-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), coq-tex(1), coqdep(1).
The Coq Reference Manual. The Coq web site: http://coq.inria.fr

Search for    or go to Top of page |  Section 1 |  Main Index


--> COQ (1) October 11, 2006

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with manServer 1.07.