Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages


home | help
COQ(1)			    General Commands Manual			COQ(1)

       coqtop -	The Coq	Proof Assistant	toplevel system

       coqtop [	options	]

       coqtop  is  the	toplevel system	of Coq,	for interactive	use.  It reads
       phrases on the standard input, and prints results on the	standard  out-

       For batch-oriented use of Coq, see coqc(1).

       -h, --help
	      Help. Will give you the complete list of options accepted	by co-

       -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-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 path
	      load Coq library path (Require path.)

       -require	path
	      load Coq library path and	import it (Require Import path.)

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

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

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

	      set sort Set impredicative

	      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)

       coqc(1),	coq-tex(1), coqdep(1).
       The Coq Reference Manual.  The Coq web site:

			       October 11, 2006				COQ(1)


Want to link to this manual page? Use this URL:

home | help