Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] CoqIDE loadpath error for ssreflect


Chronological Thread 
  • From: David Black <dtinblack AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] CoqIDE loadpath error for ssreflect
  • Date: Thu, 11 Jun 2015 10:12:07 +0100

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