The Coq mailing list

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

Dear John and Pierre,

If I am not mistaken, I believe the current working directory used to be
handled by default, hence I did not use to have a _CoqProject file. But
you are indeed right that it is just what I needed.

Thanks a lot for the help,
Best,
Yannick Zakowski

Le 29/10/2015 08:43, Pierre Courtieu a écrit :
> Hi, it should be compatible. How do you give arguments to coqtop in
> Proofgeneral? Are you sure it is not using -I? Maybe a "file variable"
> not updated?
> 
> The recommended way of setting coqtop options in pg is now via
> the _CoqProject file.
> 
> Best
> Pierre Courtieu
> 
> Le mercredi 28 octobre 2015, Yannick 
> <yannick.zakowski AT irisa.fr
> <mailto:yannick.zakowski AT irisa.fr>>
>  a écrit :
> 
>     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
>