coqchk - verify compiled Coq libraries

coqchk  is  the  standalone  checker of compiled libraries (.vo files produced by coqc) for the Coq Proof
       Assistant.  See the ReferenceManual 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.

       coqchk - verify compiled Coq libraries

-Idir,--includedir
              Add directory dir to the include path.

       -Qdircoqdir
              Map physical dir to logical coqdir.-Rdircoqdir
              Synonymous to -Q.

       -silent
              Be less verbose.

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

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

       -coqlibdir
              Overrides the default location of the standard library.

       -where Print coqchk standard library location and exit.

       -h, --help
              Print list of options.

coqtop(1), coqc(1), coq_makefile(1), coqdep(1)

       TheCoqReferenceManual.

       The Coq web site: http://coq.inria.frCOQCHK(1)

coqchk [ options ] modules