NAME

       coqchk - The Coq Proof Checker compiled libraries verifier

SYNOPSIS

       coqchk [ options ] 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.

       modules  is  a  list  of  modules  to be checked. Modules can be referred to by a short or
       qualified logical name, or by their filename.

OPTIONS

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

       -Q dir coqdir
              map physical dir to logical coqdir

       -R dir coqdir
              synonymous for -Q

       -silent
              makes coqchk less verbose.

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

       -norec 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 accept libraries that have been compiled with this flag.

       -v     print coqchk version and exit.

       -coqlib dir
              overrides the default location of the standard library.

       -where print coqchk 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

                                           July 7, 201                                     COQ(1)