coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone
Chronological Thread
- From: Stefan Monnier <monnier AT IRO.UMontreal.CA>
- To: Andrej Bauer <andrej.bauer AT andrej.com>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone
- Date: Fri, 13 Apr 2018 08:01:10 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=monnier AT IRO.UMontreal.CA; spf=SoftFail smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT pruche.dit.umontreal.ca
- Ironport-phdr: 9a23:GDnuQhwqe/FOUHTXCy+O+j09IxM/srCxBDY+r6Qd2+sRIJqq85mqBkHD//Il1AaPAd2Araocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HdbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPQNtfWS9PAo2ybYQAAeUOMvpDoonhu1cDtweyCRW2Ce/zzDJDm3/43bc90+QkCQzIwRAgEMwAsHvOqtX+KaAcUeezzKnOzDXMcelW0ir65YjNdRAhp/eMXbNufsrL0kQhFB/LgEyKpYPrOD2V0eINs3SB7+V+T+2vj3Qrph9trzW2wMonl4rHhpoNx1zZ+yh13pw5KcOkREN0e9KoDpRduiCAO4doXM8uW3xktSgkxrEcp5K3YCcHxI45yxPdcfCLbYeF7gzlWe2MOzl3nmhld6i6hxuq8Uiv1On8Vs6s3VZStCpFj8XDtnAT2BDJ98eHS+d98l282TaK0ADT7P1EIVoqmqXBL54t2KI/mYALvUTCGC/5hln2gbeLekgq5OSk8frrbqnpq5OGKYN5hQDzPr4wlsChGeg4NxIBX2mf+eSyzr3j+kj5Ta1Pjv0xlKnZtpHaKtoBpqOiAg9VyIEj5wyiDzej19QYm2UHLEhbdx2di4jlIU3BL+rgAfeln1usiCtrx+zBPrD5HprNKWHDnK79crZ59k5T0xE+zctf5pJRErEOOuj/Wk73tNzCDx82KRa4w+j9CIY16oRLcGSDGKKbeInbrFKSrrYmJeWWaY1Tsj/gJuIN7vjil3I731QaeP/684EQbSWDAvloKkPRRH3qhNYMCy9euw04Su3nknWjaxkVWlO1Wb4m6zg/TqmPW9SQDruxiaCMiX/oVqZdYXpLXxXVSS+xJte0HswUYSfXGfdP1zkNVLyvUYgkjEH8tRX9jadiKezI4CARsdTo3YouvrGBpVQJ7TVxSv+l/SSVVWgtzjEpfRhw4YV4p1Bnx16Hl4NR0aQBSI5joshRWwJ/Dqbyiux3D9eoB1DZZMqCSFvgTtS6Ryw0SdQt2dIHZwB2Eof6gw==
> It would still be better if Proof General just left the frames alone.
I believe the issue is that the frames are destroyed and re-created later.
Stefan
- [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Pierre Courtieu, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Merlin Göttlinger, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Pierre Courtieu, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Stefan Monnier, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Gaëtan Gilbert, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
- Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone, Andrej Bauer, 04/13/2018
Archive powered by MHonArc 2.6.18.