Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Vadim Zaliva <vzaliva AT cmu.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] math-classes and Coq 8.5
  • Date: Tue, 1 Mar 2016 14:07:39 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=None smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f54.google.com
  • Ironport-phdr: 9a23:QkmtxhWDT+cvo7cc+P3OhX5GuUfV8LGtZVwlr6E/grcLSJyIuqrYZheEt8tkgFKBZ4jH8fUM07OQ6PC/HzNYqs/d6TgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2MJVoQz2PhOPtbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN/dwcbsNBzM/dmsx+cfDtB/ZTALJ6GFPfH8Rl092CgTE6VnIV5PwrCKy4vRv0S2bI8TeRrUpHzmu8vE4G1fTlC4bOmthoynsgctqgfcDrQ==
Thanks for the pointers. I was checking in coq-bench and somehow it does not show 8.5 compatibility:

 https://coq-bench.github.io/


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


On Tue, Mar 1, 2016 at 1:44 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:
It seems that the Coq team has been very generously maintaining a fairly recent version of MathClasses, as Coq evolves :


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



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
Skype: vzaliva




Archive powered by MHonArc 2.6.18.

Top of Page