Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] CoqIDE loadpath error for ssreflect

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] CoqIDE loadpath error for ssreflect


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] CoqIDE loadpath error for ssreflect
  • Date: Thu, 11 Jun 2015 11:17:16 +0200

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




Archive powered by MHonArc 2.6.18.

Top of Page