The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

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"
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France


On Monday 16 July 2012 17:15:14 Alan Schmitt wrote:
> 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