coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] issue with -R option, Vladimir Voevodsky, 01/02/2014
- Re: [Coq-Club] issue with -R option, Guillaume Melquiond, 01/02/2014
- Re: [Coq-Club] issue with -R option, Vladimir Voevodsky, 01/02/2014
- Re: [Coq-Club] issue with -R option, Guillaume Melquiond, 01/02/2014
Archive powered by MHonArc 2.6.18.