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 13:11:43 -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:FDGvqRfY0Sc9mEjG7lu7Ti50lGMj4u6mDksu8pMizoh2WeGdxc6+Yx7h7PlgxGXEQZ/co6odzbGG4uaxASdZuM7JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviqtuCO04R3WL1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDuR7JBgXD8CbCX4u09wD+v/dx1S3SacbyQLU5Xyjk96Z3YBDtgSYDcTU+9TeE2YRLkKtHrUf59FREyInObdTNOQ==

On 2016-06-17 12:47, Jonathan Leivent wrote:

> How about a real-time extraction window? This was started, but not
> completed.
> I think the last time I checked there were issues on the Coq side in that
> what
> it was sending was a non-optimized extraction - what the window showed was
> much larger/complex than what would be extracted via the Extraction command
> when the definition was finished.

This is complete on the PG side IIRC (in company-coq, technically). The
remaining aspects are on the Coq side, right?

Attachment: signature.asc
Description: OpenPGP digital signature

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