The Coq mailing list

[Ranjani Krishnan <ranjani141 AT gmail.com>]

Thank you.  I installed coq 8.5. But when I try to compile my file, it gets stuck at 'running..' 

How do I know if the compilation was successful?

On Tue, Feb 9, 2016 at 3:18 PM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Tue, Feb 09, 2016 at 07:02:43AM +0530, Ranjani Krishnan wrote:
> I am new to coq. When I tried to do 'Require ssreflect.ssreflect' I am
> getting the compilation error : "File
> E:\Coq\lib\user-contrib\mathcomp/Ssreflect/ssreflect.vo
> has bad magic number. It is corrupted or was compiled with another version
> of
> Coq"
>
> I am using the coq ide for windows version 8.4pl6. Can someone help me
> solve this?

I guess you installed mathcomp/ssreflect with the installer provided at
  http://math-comp.github.io/math-comp/

Unfortunately such installers work only for Coq 8.5.

What I suggest is that you upgrade Coq to 8.5, see the installers here:
  https://coq.inria.fr/download

Best,
--
Enrico Tassi

--

Thanks,

Ranjani