Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] issue with -R option

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] issue with -R option


Chronological Thread 
  • From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] issue with -R option
  • Date: Thu, 02 Jan 2014 00:23:26 +0100

On 02/01/2014 00:14, Vladimir Voevodsky wrote:

This also feels like a bug.

No, both behaviors are fine; they are intended.

When you execute "coqc what/ever/a", the resulting module is just "a". So if you import "something.a", you get a mismatch.

When you execute "coqc -R . something what/ever/a", the resulting module is "something.what.ever.a".

And if you execute "coqc -R what something what/ever/a", the resulting module is "something.ever.a". So, in your case, you want to use "coqc -R Test Test Test/a" so that the resulting module is "Test.a".

Best regards,

Guillaume



Archive powered by MHonArc 2.6.18.

Top of Page