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.
A big thanks to the people on the Coq-Club Forum who helped with this problem, and in particular Pierre Boutillier who pinpointed the cause of the problem and provided the solution.
The problem was that I had 2 copies of coqtop and 2 copies of standard libraries:
Therefore when I was in CoqIDE it was calling a different version of coqtop than the one that I used to compile and install the Ssreflect library.
The solution is the following :
I successfully loaded the Ssreflect library both using coqtop in the Terminal and CoqIDE using: