coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ralf Jung <jung AT mpi-sws.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] CoqIDE loadpath error for ssreflect
- Date: Thu, 11 Jun 2015 13:05:03 +0200
Hi David,
> 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.
My first guess would be to change the LoadPath to
Add LoadPath "/opt/local/lib/coq/user-contrib/".
The "Ssreflect" is already part of the module name that's loaded, so
this could fix the naming mismatch Coq is seeing.
Kind regards,
Ralf
- [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, Enrico Tassi, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Pierre Boutillier, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 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.