coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] math-classes and Coq 8.5

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] math-classes and Coq 8.5
Date: Tue, 1 Mar 2016 16:44:27 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f176.google.com
Ironport-phdr: 9a23:nLhwhhfT5CbPIO5VdafBE/zrlGMj4u6mDksu8pMizoh2WeGdxc68ZB7h7PlgxGXEQZ/co6odzbGG7Oa/ASdZvc/JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuMO04R2GP1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/rJngsgCGRg+S7FMdVH8Xm1xGGV6Wwgv9W8LYuCv7repw22GzO8TwQfhgUD6i7rxrRRyugSEOMTJ/8WDLheR/iatapFSqoBkpkN2cW52cKPcrJvCVRtgdX2cUBss=

It seems that the Coq team has been very generously maintaining a fairly recent version of MathClasses, as Coq evolves :

https://scm.gforge.inria.fr/anonscm/git/coq-contribs/math-classes.git

I was able to fully compile the v8.5 branch in Coq 8.5.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, Mar 1, 2016 at 3:02 PM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

I am wondering if anybody is working on porting math-classes to coq-8.5. I recall Abhishek ported the parts he needs. Perhaps other people also worked on this and we can combine our efforts. I am not up to the tasks myself, but I can try to assist in any way I could.

Vadim

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060
Skype: vzaliva

[Coq-Club] math-classes and Coq 8.5, Vadim Zaliva, 03/01/2016
- Re: [Coq-Club] math-classes and Coq 8.5, Beta Ziliani, 03/01/2016
- Re: [Coq-Club] math-classes and Coq 8.5, Abhishek Anand, 03/01/2016
  - Re: [Coq-Club] math-classes and Coq 8.5, Vadim Zaliva, 03/01/2016