gallina(1) [debian man page]

COQ(1)							      General Commands Manual							    COQ(1)

NAME

       gallina - extracts specification from Coq vernacular files

SYNOPSIS

       gallina [ - ] [ -stdout ] [ -nocomments ] file ...

DESCRIPTION

       gallina	takes  Coq files as arguments and builds the corresponding specification files.  The Coq file foo.v gives bearth to the specifica-
       tion file foo.g. The suffix '.g' stands for Gallina.

       For that purpose, gallina removes all commands that follow a "Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until  it	reaches  a
       command "Abort.", "Save.", "Qed.", "Defined." or "Proof <...>.". It also removes every "Hint", "Syntax", "Immediate"  or "Transparent" com-
       mand.

       Files without the .v suffix are ignored.

OPTIONS

       -stdout
	      Prints the result on standard output.

       -      Coq source is taken on standard input. The result is printed on standard output.

       -nocomments
	      Comments are removed in the *.g file.

NOTES

       Nested comments are correctly handled. In particular, every command "Save." or "Abort." in a comment is not taken into account.

BUGS

       Please report any bug to coq@pauillac.inria.fr

Coq tools							   29 March 1995							    COQ(1)

COQ(1)							      General Commands Manual							    COQ(1)

NAME

       coqchk - The Coq Proof Assistant compiled libraries verifier

SYNOPSIS

       coqchk [ options ] files-or-modules

DESCRIPTION

       coqchk  is  the standalone checker of compiled libraries (.vo files produced by coqc) for the Coq Proof Assistant. See the Reference Manual
       for more information. It returns with exit code 0 if all the requested tasks succeeded. A non-zero return code means  that  something  went
       wrong: some library was not found, corrupted content, type-checking failure, etc.

       files-or-modules  is  a list of modules to be checked. Modules can be referred to either by a filename (without the .vo suffix) or by their
       (possibly qualified) module name.

OPTIONS

       -I dir, --include dir
	      add directory dir in the include path

       -R dir coqdir
	      recursively map physical dir to logical coqdir

       -where print Coq's standard library location and exit

       -silent
	      makes coqchk less verbose.

       -admit file-or-module
	      tag the specified module and all its dependencies as trusted, and will not  be  rechecked,  unless  explicitly  requested  by  other
	      options.

       -norec file-or-module
	      specifies that the given module shall be verified without requesting to check its dependencies

       -m, --memory
	      displays a summary of the memory used by the checker

       -o, --output-context
	      displays a summary of the logical content that have been verified: assumptions and usage of impredicativity

       -impredicative-set
	      allows the checker to verify libraries that have been compiled with this flag.

       -v     print Coq version and exit

       -where print Coq's standard library location and exit

       -h, --help
	      print list of options

SEE ALSO

       coqtop(1), coqc(1), coq_makefile(1), coqdep(1).
       The Coq Reference Manual.  The Coq web site: http://coq.inria.fr

								 February 9, 2009							    COQ(1)