The Coq Proof Assistant, version 8.6 (July 2017) compiled on Jul 27 2017 8:50:48 with OCaml 4.04.0

Usage: coqc <options> <Coq options> file... options are: -verbose compile verbosely -image f specify an alternative executable for Coq -opt run the native-code version of Coq -byte run the bytecode version of Coq -t keep temporary files Coq options are: -I dir look for ML files in dir -include dir (idem) -R dir coqdir recursively map physical dir to logical coqdir -Q dir coqdir map physical dir to logical coqdir -top coqdir set the toplevel name to be coqdir instead of Top -notop set the toplevel name to be the empty logical path -exclude-dir f exclude subdirectories named f for option -R -noinit start without loading the Init library -nois (idem) -compat X.Y provides compatibility support for Coq version X.Y -load-ml-object f load ML object file f -load-ml-source f load ML file f -load-vernac-source f load Coq file f.v (Load f.) -l f (idem) -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.) -lv f (idem) -load-vernac-object f load Coq object file f.vo -require path load Coq library path and import it (Require Import path.) -compile f.v compile Coq file f.v (implies -batch) -compile-verbose f.v verbosely compile Coq file f.v (implies -batch) -o f.vo use f.vo as the output file name -quick quickly compile .v files to .vio files (skip proofs) -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio into fi.vo -schedule-vio-checking j f1..fn run up to j instances of Coq to check all proofs in each fi.vio -where print Coq's standard library location and exit -config, --config print Coq's configuration information and exit -v print Coq version and exit -list-tags print highlight color tags known by Coq and exit -quiet unset display of extra information (implies -w "-all") -w (w1,..,wn) configure display of warnings -color (yes|no|auto) configure color output -q skip loading of rcfile -init-file f set the rcfile to f -batch batch mode (exits just after arguments parsing) -boot boot mode (implies -q and -batch) -bt print backtraces (requires configure debug flag) -debug debug mode (implies -bt) -emacs tells Coq it is executed under Emacs -noglob do not dump globalizations -dump-glob f dump globalizations in file f (to be used by coqdoc) -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes) -impredicative-set set sort Set impredicative -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives -type-in-type disable universe consistency checking -xml export XML files either to the hierarchy rooted in the directory $COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset) -time display the time taken by each command -profile-ltac display the time taken by each (sub)tactic -m, --memory display total heap size at program exit (use environment variable OCAML_GC_STATS="/tmp/gclog.txt" for full Gc stats dump) -native-compiler precompile files for the native_compute machinery -h, -help, --help print this list of options