The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Hi Adam,

Thanks for the hints, now everything is ok.

Regards,

Marcus.

2013/11/8 Adam Chlipala <adamc AT csail.mit.edu>

On 11/08/2013 10:03 AM, Marcus Ramos wrote:

Thanks Adam, but I still can´t make it. I´ll try to be more specific then:

I have a file name "Automata.v" which is located at "C:\Users\Marcus Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current\Sources". This file starts with the following lines:

(*--------------------*)

Require Import Ascii.

Require Import String.

Require Import NPeano.

Add LoadPath "C:\Users\Marcus Ramos\Documents\UFPE\CIn\Doutorado\Tese\Current" as Current.

I recommend never using "Add LoadPath."  Essentially I'm suggesting ignoring source file management commands not described in that chapter of CPDT.  This may be an unsatisfying answer from the standpoint of particular questions you have about those other commands, but I think it sets you on the best practical path.

When I execute "coqdep *.v" at Sources, I get the messages (besides others):

I suggest never running "coqdep" directly.  I've never done it myself, so it's not just that I'm trying to discourage you from using an "advanced" feature until you've learned more. ;)  coq_makefile encapsulates the important features nicely.