coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files
Date: Thu, 31 Jan 2019 10:28:01 +0100

On Wed, 2019-01-30 at 16:44 -0800, Abhishek Anand wrote:
> I deleted a .v file and forgot to remove it from `_CoqProject`.
> Suddenly, I was getting too many errors that indicated that `make` is
> trying to compile files in an order that disrespects the
> dependencies.

Hi Abhishek, could you please confirm the bug is
the same reported here:

https://github.com/coq/coq/issues/9319

If not, please open another issue with your example.

Best,
--
Enrico Tassi

[Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Abhishek Anand, 01/31/2019
- Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Enrico Tassi, 01/31/2019
  - Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Abhishek Anand, 01/31/2019