Ssreflect Users Discussion List

[Laurent Théry <>]

On 10/10/2012 11:32 AM, Beta Ziliani wrote:
> Hi list,
>
> I have the following not so important yet annoying problem.
>
> Usually people compile coq and then ssreflect, in this order, and this
> works fine. But in my case, I sometimes need to go back and recompile
> Coq. Then, the following error message appears:
>
> File "coq/theories/Bool/Bvector.v", line 12, characters 0-15:
> Error: The file coq/user-contrib/Ssreflect/Vector.vo contains library
> Ssreflect.vector and not library Ssreflect.Vector
>
> which means that Coq is preferring the vector library from ssreflect
> than its own.
>
> What I do to overcome this problem is to rename user-contrib, compile
> Coq, and rename it back. But I suppose there's a better way of dealing
> with this problem. Any suggestions?
>
> Thanks,
> Beta
>
> P.S.: Wouldn't it be better to have ssreflect's vector renamed to
> ssrvector to avoid this name clashes?

This is strange, The file coq/user-contrib/Ssreflect/Vector.vo
should be /user-contrib/Ssreflect/vector.vo. Which operating system
are you  using?

--
Laurent