coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Suggestions for Proof General?

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Fri, 17 Jun 2016 11:47:38 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:BpI+HRXTMUOepd5Kql+BAjoiT1zV8LGtZVwlr6E/grcLSJyIuqrYZhCCt8tkgFKBZ4jH8fUM07OQ6PCxHz1Yqsfb+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8yVMl0D1WD1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDuR7JBgXD8CbCX4u09wD+v/dx1S3SacbyQLU5Xyjk96Z3YBDtgSYDcTU+9TeE2YRLkKtHrUf59FREyInObdTNOQ==

On 2016-06-17 11:30, Emilio Jesús Gallego Arias wrote:
> The only downside that is the whole proof will have to be run, but I'm
> sure there could be a fast mode.

I don't think that'll be an issue, right? The output can be cached at
publication time.

Attachment: signature.asc
Description: OpenPGP digital signature

Re: [Coq-Club] Suggestions for Proof General?, (continued)