coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [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:15:16 +0200

Hello,

I'm having a strange error that appeared after I recompiled coq. I'm using
the flocq library in some project, so I compile it locally (I don't install
it anywhere), but when I need to use it I get this error

coqc -I . -I js -I tlc -I flocq/src/Core -I flocq/src/Calc -I flocq/src/Appli
-I flocq/src/Prop -I tlc js/JsNewSyntax.v
File "/Users/schmitta/projets/jscert/coq/js/JsNewSyntax.v", line 6,
characters 0-37:
Error: The file
/Users/schmitta/projets/jscert/coq/flocq/src/Appli/Fappli_IEEE.vo contains
library
Flocq.Appli.Fappli_IEEE and not library Fappli_IEEE

I tried recompiling everything, but I always get this error. I'm using coq
8.3pl4.

If someone has a suggestion, I'm running out of ideas to get around this.

Thanks,

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