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: Andrej Bauer <andrej.bauer AT andrej.com>
  • To: Pierre Courtieu <pierre.courtieu AT gmail.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 15:33:21 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=andrej.bauer AT andrej.com; spf=None smtp.mailfrom=andrej.bauer AT andrej.com; spf=None smtp.helo=postmaster AT mail-io0-f181.google.com
  • Ironport-phdr: 9a23:RIucGBzbcfi2oyrXCy+O+j09IxM/srCxBDY+r6Qd2+8fIJqq85mqBkHD//Il1AaPAd2Araocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HdbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRGpOXMhRWSxPDI2/coUBEfYOMP1Er4XhvVYCsQeyCRWuCe7p1zRGhmX23ao/0+k5DQzG2hEvH8gQv3TWsd74Kb0dUf2rw6nS0D7OaOlZ2THg54jSbB8ho+uAUqlqfsrM10YvDRjIgU+WqYP4JTOayOYNv3KH4OpnUOKikmgqoBxyrDi33soglJXFi4YPxl3H9Sh12pg5KcO2RUJhfNKpE4ZcuzmEO4dqXs8uXmRltDs1x7AEpZK2eSYKyJopxxLDbvGKcIaF7g7mWemMPTh3mG5pdbe7ihuy7USs1ujxWte73VlQqidIl9fBu3IX2BHd7MWMV+Fz8V272TmV0gDe8uFELl4wlarcM5Mhx6Q/lpsXsUjaHy/2n1n6gLaYdkk5+eWk9v7rYrrhpp+bOI90jh/xPr4ylcy4BOQ0KgkOX26F9uSgzLDv41H1TbFQgvA1kqTVqo7WKdoVq6KjHgNY0Zsv5w66Dzi80dQYmXcHLEhCeBKCl4XmIVfOL+3iDfihgVSgiixkyOrbPrL/GJXANWLMkLH8crZn9UFcyhA/wsxY55JREr0BOu78WlfttNzECR80KxC7w+H+CNlkyoweXX+PDbSCPaPJsV6I4/ovLPOWaI8Uvjb9Mfkl6OT0gX83g19ONZWuiKMWZWqiE7xNJFiDfXvhn59VCWYHpBAzCuftlUeeUDNOT3m3VqM4oDo8DdT1I53EQ9WEhrCb0SXzNJRLa3oOXlmKHW3ldcOOUuoBcgqbJMN7nz5CXr+kHdxynSqyvRP3nuI0ZtHf/TcV4Ne6jIAstr/j0Coq/DkxNPyzlmSETmV6hGQNHmVk1aZzu0F/jFyE1Pog2qAKJZlo//pMFzwCG9vE1eUjUYL7XA7bc9XPQ1GjEI3/XGMBC+kpytpLWH5TXtWviheZgXivCr4R0r2MXNk6q/KFmXf2IMl5xjDN06xz11Q=

> For the latter it would help to know in which scenario you need to restart
> coq.

Decativating coq because we're starting a fresh one in another buffer
is the common case when we don't want the existing frames to disappear
and re-appear.



Archive powered by MHonArc 2.6.18.

Top of Page