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

FreeBSD Manual Pages

  
 
  

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

NAME
       coqide -	The Coq	Proof Assistant	graphical interface

SYNOPSIS
       coqide [	options	]

DESCRIPTION
       coqide is a gtk graphical interface for the Coq proof assistant.

       For  command-line-oriented  use	of Coq,	see coqtop(1) ;	for batch-ori-
       ented use of Coq, see coqc(1).

OPTIONS
       -h     Show the complete	list of	options	accepted by coqide.

       -I dir, -include	dir
	      Add directory dir	in the include path.

       -R dir coqdir
	      Recursively map physical dir to logical coqdir.

       -src   Add source directories in	the include path.

       -nois  Start with an empty state.

       -load-ml-object f
	      Load ML object file f.

       -load-ml-source f
	      Load ML file f.

       -l f, -load-vernac-source f
	      Load Coq file f.v	(Load f.).

       -lv f, -load-vernac-source-verbose f
	      Load Coq file f.v	(Load Verbose f.).

       -load-vernac-object path
	      Load Coq library path (Require path.).

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

       -compile	f
	      Compile Coq file f.v (implies -batch).

       -compile-verbose	f
	      Verbosely	compile	Coq file f.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 f
	      Set the rcfile to	f.

       -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 f
	      Dump globalizations in file f (to	be used	by coqdoc(1)).

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

SEE ALSO
       coqc(1),	coqtop(1), coq-tex(1), coqdep(1).
       The  Coq	 Reference  Manual,  The  Coq  web  site: http://coq.inria.fr,
       /usr/share/doc/coqide/FAQ.

AUTHOR
       This manual page	 was  written  by  Samuel  Mimram  <samuel.mimram@ens-
       lyon.org>, for the Debian project (but may be used by others).

				 July 16, 2004			     COQIDE(1)

NAME | SYNOPSIS | DESCRIPTION | OPTIONS | SEE ALSO | AUTHOR

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=coqide&sektion=1&manpath=FreeBSD+12.1-RELEASE+and+Ports>

home | help