Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to tell proof general to leave the *response* and *goal* frames alone

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:23:05 -0400
  • Authentication-results: mail3-smtp-sop.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 chene.dit.umontreal.ca
  • Ironport-phdr: 9a23:NfcLXBO3Cd5A8zjxRhgl6mtUPXoX/o7sNwtQ0KIMzox0Iv3+rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZXshfSTFPDICyb4UBDeUOM+lXoJXmqlsSsRezHxWgCP/1xzNUgHL9wK000/4mEQHDxAEuAs4Ov2rarNrvMqcZTOe7zK7OzTXFbvNZxy3945XPfxAkpvGMW7RwccvPxkk1DA7LjUmep5X/Mzyb0eoNtG6b7/Z6Ve2xkWEnrxt9ryazy8o1jITCm4Ebykjc+Clkzos5O8e0RFBnbdOrCpdcqS6XOopsTs88X21koDs2x7MYtZKhYiQG1JsqywTBZ/GFaYSE/B3uWPiXLDxlnnxqYqi/iAy38UW4yu3zSM200FFSoyVZktnDqHYN2ALJ5seaS/t94l2t2SuK1wDU7OFEPVo0mrTBJJ4l2LI/ioAcvVzCHi/whkr2kLebelgq9+S28ejrfKnqq5CGO4NqhQzzM74iltKjDeggNwgBRWmb+eCy1L35+k35Ra1HjvgxkqnftpDaJNoUprSiDg9UyIYj7AyzDyqj0NQfm3kHMEhFdwydgIjtIV3BPOr3Ae+lg1uwiDdr2+zGPrr5D5rRKXjDia7tcqp5605B0wU+1stf5pJRCrEZOv3/QE7xtNrCDh84KQO42ejnCM8unr8ZDEuJDrWUMuv4uEKF/Kp7Ku+AfoIX/jz0NvU/z/fogWU0mxkWeqz/jrUNb3XtJehrLUyfKV/rhNEAHH1C6g85SurrhUeqcAR0IUuXWKQg/DwyDMSNJNGQFciWnLWd0XLjTdVtbWdcBwXJSC+wLtTWa7I3cCuXZ/RZvHkBXLmlRZUm0Ej+5g7gzPx6K+3S5jcVvJal39EnvLSPxyF3ziR9CoGm60/IV3t9xzNaZgURmp1apkph0FqK1e5Tqq4ATIEB17ZySg4/cKXk4al6BtT1AF6TddeETlvgTtS6Ryw0SdQt2dIHZwB2Eof6gw==

> 3. when the Coq process dies, so do the associated buffers.

This is done by Proof-General, not by Emacs, so that should be "easy" to fix.


Stefan



Archive powered by MHonArc 2.6.18.

Top of Page