coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Error about a file containing a library with a fully qualified name instead of just the name

From: Alan Schmitt <alan.schmitt AT polytechnique.org>
To: Coq <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Error about a file containing a library with a fully qualified name instead of just the name
Date: Mon, 16 Jul 2012 17:29:06 +0200

On 16 juil. 2012, at 17:21, Paolo Herms wrote:

> Hello Alan,
> it seems you compiled the library with the -R option and now you're trying
> to
> use it with an -I option.
> Try to replace all your "-I flocq/src/..." with something like
> "-R flocq/src/ Flocq"

That was it. Thanks a lot !

Alan

[Coq-Club] Error about a file containing a library with a fully qualified name instead of just the name, Alan Schmitt, 07/16/2012
- Re: [Coq-Club] Error about a file containing a library with a fully qualified name instead of just the name, Paolo Herms, 07/16/2012
  - Re: [Coq-Club] Error about a file containing a library with a fully qualified name instead of just the name, Alan Schmitt, 07/16/2012