FreeBSD Manual Pages
COQTOP(1) General Commands Manual COQTOP(1) 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). OPTIONS -h, --help Help. Will give you the complete list of options accepted by coq- top. -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)). -impredicative-set Set sort Set impredicative. -dont-load-proofs Don't load opaque proofs in memory. SEE ALSO coqc(1), coq-tex(1), coqdep(1) The Coq Reference Manual. The Coq web site: http://coq.inria.fr COQTOP(1)
NAME | SYNOPSIS | DESCRIPTION | OPTIONS | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=coqtop&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>