coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] math-classes and Coq 8.5
Date: Tue, 1 Mar 2016 17:29:47 -0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:uhvJIRVRX6Na4JSavoMC0PtqznXV8LGtZVwlr6E/grcLSJyIuqrYZhKAt8tkgFKBZ4jH8fUM07OQ6PC/HzNYqs/a7TgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2MJVoQz2PmPPtbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN4xxd7FTDSwnPmYp/4Wr8ECbFUrcrkcbB04Ri1JjBxXPpEXxWY60uS/nvMJ83jObNIv4V+Zndy6l6vJBRQPhwBUGMz8w9mCf3sZ9kKtzpQqg4gdg2MjTeo7DZ6k2Rb/UYd5PHTkJZc1WTSEUR9rkN4Y=

See http://coq-club.inria.narkive.com/uy4GsR8S/8-5-and-mathclasses

On Tue, Mar 1, 2016 at 5: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