The Coq mailing list

[flaviomoura AT unb.br (Flávio L. C. de Moura)]

Hello Coq users,

I am facing a strange problem with Proof General, and I didn't realize
how to solve it. When I try to process a .v file (with Coq 8.4pl4), I
get the following screen:

Don't know what to do with -Q
Usage: coqtop <options>

Coq options are:
  -I dir -as coqdir      map physical dir to logical coqdir
  -I dir                 map directory dir to the empty logical path
  -include dir           (idem)
  -R dir -as coqdir      recursively map physical dir to logical coqdir
  -R dir coqdir          (idem)
  -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

  -inputstate f          read state from file f.coq
  -is f                  (idem)
  -nois                  start with an empty state
  -outputstate f         write state in file f.coq
  -compat X.Y            provides compatibility support for Coq version X.Y
  -verbose-compat-notations  be warned when using compatibility notations
  -no-compat-notations   get an error when using compatibility notations

  -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 f             load Coq object file f.vo and import it (Require f.)
  -compile f             compile Coq file f.v (implies -batch)
  -compile-verbose f     verbosely compile Coq file f.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
  -config                print Coq's configuration information and exit
  -v                     print Coq version and exit

  -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)
  -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
  -force-load-proofs     load opaque proofs in memory initially

  -lazy-load-proofs      load opaque proofs in memory by necessity (default)
  -dont-load-proofs      see opaque proofs as axioms instead of loading them
  -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
  -h, --help             print this list of options


I have opam installed, and if I switch to Coq 8.5 or 8.6, everything
works fine. The first line of the above screen says "Don't know what to
do with -Q" but I don't know how to fix this. Any help is very welcome.

Best regards,
Flávio.