The Coq mailing list

[David Black <dtinblack AT gmail.com>]

Hi Ralf,

I used the following instructions in CoqIDE:

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

Require Import Ssreflect.ssreflect.

but got the error: Cannot find library Ssreflect.ssreflect in loadpath

Also, the file ssreflect.vo is in the folder.

Kind regards,

David

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

Hi,

> 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 ) ?

Please try "Require Import Ssreflect.ssreflect".

There should be a file
/opt/local/lib/coq/user-contrib/Ssreflect/ssreflect.vo.

Kind regards,
Ralf