coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ssreflect

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ssreflect
Date: Tue, 9 Feb 2016 10:48:33 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:IE333x2YMGZRKqz+smDT+DRfVm0co7zxezQtwd8ZsegVLfad9pjvdHbS+e9qxAeQG96LtLQf06GO7ejJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZ/vnLjss7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCaJ/HoXVS0qmwFTAkCR4RfgX5z29DfzrfF88CicJ8z/C74uD2fxp5x3QQPl3X9UfwUy93va35R9

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

[Coq-Club] Ssreflect, Ranjani Krishnan, 02/09/2016
- Re: [Coq-Club] Ssreflect, Enrico Tassi, 02/09/2016
  - Re: [Coq-Club] Ssreflect, Ranjani Krishnan, 02/11/2016
    - Re: [Coq-Club] Ssreflect, Enrico Tassi, 02/11/2016
      - Re: [Coq-Club] Ssreflect, Ranjani Krishnan, 02/13/2016
        
        Re: [Coq-Club] Ssreflect, Laurent Thery, 02/13/2016
        
        Re: [Coq-Club] Ssreflect, Ranjani Krishnan, 02/14/2016