coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Suggestions for Proof General?
Date: Fri, 17 Jun 2016 13:14:38 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f177.google.com
Ironport-phdr: 9a23:cxSmdB8jfFd8Rv9uRHKM819IXTAuvvDOBiVQ1KB91+scTK2v8tzYMVDF4r011RmSDdSduqoP0rOO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt+U3pz8jrnqs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCmI4HIAUmwQ2j5FAhbI6g2yCpX2tCr5u+5w1QGVOMT3SfY/XjH0vPQjcwPhlCpSb21xy2rQkMEl1K8=

On 06/17/2016 01:11 PM, Clément Pit--Claudel wrote:

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?

I think so.

-- Jonathan

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