The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi David,

> I get the error: Cannot find library ssreflect in loadpath
> 
> I have tried using: Add LoadPath "/opt/local/lib/coq/user-
> contrib/Ssreflect/".
> 
> where SSRCOQ_LIB is currently set,
> 
> but I get the error: The file
> /opt/local/lib/coq/user-contrib/Ssreflect/ssreflect.vo
> contains library Ssreflect.ssreflect and not library ssreflect
> 
> Grateful for any help in loading the ssreflect library from within CoqIDE.

My first guess would be to change the LoadPath to

Add LoadPath "/opt/local/lib/coq/user-contrib/".

The "Ssreflect" is already part of the module name that's loaded, so
this could fix the naming mismatch Coq is seeing.

Kind regards,
Ralf