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: 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



Archive powered by MHonArc 2.6.18.

Top of Page