The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> I used the following instructions in CoqIDE:
> 
> Add LoadPath "/opt/local/lib/coq/user-contrib/Ssreflect/".

That's not what I suggested should work ;-)

Quoting from my first mail:
Add LoadPath "/opt/local/lib/coq/user-contrib/".

> Require Import Ssreflect.ssreflect.

Coq concatenates the paths: if you tell it to look in
"/opt/local/lib/coq/user-contrib/", and it looks for
Ssreflect.ssreflect, the "." becomes a "/" and a ".vo" is added. That's
the file it looks for.

The alternative would be to add "Ssreflect" to the Path *and* *not* do
the "Require", but you said that's what you tried first, and it did not
work.

Kind regards,
Ralf