The Coq mailing list

[David Black <dtinblack AT gmail.com>]

Hi Ralf,

Thanks for the suggestion.

Unfortunately when I followed the instruction I got the following error: Cannot find library ssreflect in loadpath

What file extension should the ssreflect library have ( I would like to check that it is in the folder ) ?

Kind regards,

David

On Thu, Jun 11, 2015 at 12:05 PM, Ralf Jung <jung AT mpi-sws.org> wrote:

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