coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Pierre Courtieu, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Pierre Courtieu, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Pierre Wilke, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Pierre Courtieu, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Pierre Courtieu, 06/11/2015
Archive powered by MHonArc 2.6.18.