The Coq mailing list

[Pierre Wilke <pierre.wilke AT irisa.fr>]

    Hello,
    
    Have you tried the following?
    Add LoadPath "path/to/ssreflect" as Ssreflect.
    
    It solves the same kind of problem for me (not with Ssreflect,
    though).
    
    Pierre

On 06/11/2015 11:47 AM, David Black wrote:

To load at the Terminal I use: coqtop

To run CoqIDE I click on the icon in the Application Folder ( I installed it using coqude-8.4p15.dmg ).

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

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