The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Can you give the exact way you launch coqtop (terminal) and coqide please? You should somehow set the same loadpath options for both.

P.

2015-06-11 11:27 GMT+02:00 David Black <dtinblack AT gmail.com>:

Hi Pierre,

Thanks for the suggestion which I tried but unfortunately I get the error:  Cannot find library Ssreflect.ssreflect in loadpath.

Kind regards,

David

On Thu, Jun 11, 2015 at 10:17 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Hi, welcome to Coq.

Have you just tried "Require Import Ssreflect.ssreflect." ?

Best regards,

Pierre

2015-06-11 11:12 GMT+02:00 David Black <dtinblack AT gmail.com>:

Hello,

I am a Coq newbie and therefore to improve my understanding of proof checking I am trying to use the Ssreflect library.

I have installed Ssreflect v 1.5 on a Mac OS v 10.10.3 ( Yosemite ) which runs at the Terminal.

However when I tried to load the library into CoqIDE 8.4p15 using: Require Import ssreflect.

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.

Kind regards,

David Black