On 2016-06-15 19:10, Makarius wrote:
> Yes, that is by Carst Tankink -- I was working with him over 6 months,
> before I left France. Later the Coqoon guys also joined the move,
> because I encouraged them to do that, but it never became first-class
> for Coq.

Well, it was demoed to an audience of maybe 100 people as a platform enabling 
cool new features that were not available anywhere else (in this case it was 
resilience to errors, to report more than just the first one). In any case I 
think it's a great project; thanks for making it possible!

> You see, I am somehow behind many of the prover IDE modernization
> projects, but not all of them.

I didn't mean to imply anything about how well up-to-date you are in my 
previous email; I hope it didn't give a bad impression.

> Ultimately, what counts is what really works, and what is really maintained.

Agreed.

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to