glabels-3(1) [debian man page]

glabels(1)						      General Commands Manual							glabels(1)

NAME

       glabels - Label and business card creation program for GNOME

SYNOPSIS

       glabels-3 [OPTIONS] [label-filename...]

       glabels-3-batch [OPTIONS] [label-filename...]

DESCRIPTION

       glabels-3  is  a  lightweight program for creating labels and business cards for the GNOME desktop environment. It is designed to work with
       various laser/ink-jet peel-off label and business card sheets that you'll find at most office supply stores.  glabels-3	is  pre-configured
       with  templates for many of these products.  It also provides an interactive template designer for creating new templates according to user
       specifications.

       For full documentation see the gLabels online help.

       glabels-3-batch is a command line utility to print labels previously prepared with glabels-3.

OPTIONS

       -?, --help
	      Display a summary of available command-line options.

       --usage
	      Display a short usage summary.

       -v, --version
	      Print program version information.

       Options specific to glabels-batch

       -o filename, --output=filename
	      Set output filename to filename. (default="output.ps")

       -i filename, --input=filename
	      Set name of file with data to be merged to filename. Typically this is a .csv file containing values to be printed on the labels.

       -s n, --sheets=n
	      Set number of sheets to n. (default=1)

       -c n, --copies=n
	      Set number of copies to n. (default=1)

       -f n, --first=n
	      Set label on first sheet to start printing from to n. (default=1)

       -l, --outline
	      Print outlines around labels.  This is useful for testing printer alignment or printing proof sheets.

       -C, --cropmarks
	      Print crop marks. Helpful for cutting up sheets.

       -r, --reverse
	      Print mirror image of labels.  This is useful for clear labels intended to be seen from the back through glass.

FILES

       The $HOME/.glabels directory contains all user-defined templates.

SEE ALSO

       The gLabels homepage at <http://glabels.org/>.

AUTHOR

       Jim Evins <evins@snaught.com>

								   Jun 28, 2004 							glabels(1)

COQ(1)							      General Commands Manual							    COQ(1)

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 out-
       put.

       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

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

       -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

								 October 11, 2006							    COQ(1)