Ssreflect Users Discussion List

[Beta Ziliani <>]

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?