The Coq mailing list

[Yannick <yannick.zakowski AT irisa.fr>]

Dear all,

Following my previous question, I switched to the 8.5b2. I however have
an issue with coqdep: it seems that the behaviour of the -I option has
changed.
Having a file foo.v, and a Require Import foo. in another file bar.v,
the following command now fails:
coqdep -I . bar.v
But it now works with a -Q or -R option.
However, it seems that Proof General did not adapt to this change, since
trying to interpret the Require Import calls coqdep with -I and fails.
What is a bit more surprising is that it seems that this has been
considered since a change to the function "coq-find-project-file" in the
coq.el file has been made to remove any use of the obsolete -I -as
option, in the 4.3pre150930 version.
Hence the question: am I missing something or was the change partial and
is Proof General currently incompatible with Coq 8.5b2?

Thanks for your help,
Best,
Yannick