coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] displaying goal and hypotheses

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] displaying goal and hypotheses
Date: Wed, 14 Nov 2018 23:19:21 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:31hRiRXHgpyiR0VA5EYOI+6PkZTV8LGtZVwlr6E/grcLSJyIuqrYbBOFt8tkgFKBZ4jH8fUM07OQ7/i/HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9wIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kb5brhyiqRx+34Hab46aOeFifqzGZ94WWXZNUtpTWiFHH4iyb5EPD+0EPetAq4fyuUEOogW7BQisGejhxCVHh3Ht3a091eQqDAbL0gg+ENIUrnvUqdX0OL0cX++vwqjI1jLDb/VN1Djn7ojIbwotru+RUrJta8be01QvGhrDg16NqoLlJyuY2+sRv2SB8uZsSeCih3Q6pwx/ozWj3NoghpXJi44N11zJ9Tl1zJwrKdGkRkN3e8CoHIZMuy2AKod7TMcvT3lmuCkkybAKpZu2cS0EyJs6yRPTdvmKfoyG7x/hWuacJCp3iXBmdb2jghu97FWvxfDgWcSyzV1EtDBKksPWuXAIzxHT6taISv96/kq5xTuA2R3d5v1ZLUwtkqTVJIMtzqc3lpUIr0vPBCj2mFjqjKCNcUUk5+6o5Pn9brX+vJ+cMJN0hR/iPaQym8y/BuI4PhIJX2iG5eS80Lrj/Ur6QLlQkvI2lazZvIjbJcQduKG5HxdY34k/5xqlEjuqzNYVkWMaIF9LeR+LlZXlN03OLfzgCPewmVWskDNlx/DcOb3hB43AIHzdn7f7Y7l97k5dxBA9w99F6ZNUEbYBIPToV0DrstzYEwU1PBKpzOb6EtlyzJ4eVXqVAqCFKKPSrUOI5uU3LuaQY48VoS/xJOQh5/7zlnA0gkQdfKms3ZsPcn+0BPVmI0ODYXrtmNgNC2kKvhBtBNDt3ReJVicWbHKvVYo94Cs6AcSoF82LEouqmfmK2DqxNpxQfGFPTF6WRyTGbYKBDtUBci+XM4dNmyMfUr7pH60szxyrpUnWwqV8Kez88ysF85/vyZ58+ruAxlkJ6TVoApHFgCm2RGZukzZQHm5k7OVEuUV4j2y7/+19iv1cG8ZU4qoTAA48KNjRw/E8As2gA1udLOfMc06vR5CdOR90Vsg4moVcakBgXdiuk1bKwnjyWuJHp/mwHJUxt5nk8T3xKsJ6lymU/ZQa1wBjZ+YWcGqsi+h46hTZAJPPnwOBjaG2eK8A3SnLsmCe0W6Ju0IeWwl1A/zI
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi coq-club,

thanks for all the answers to my previous question

sometimes I find coq gets into a state where when I apply a tactic, the
new goal and hypotheses don't automatically get displayed. How do I
reset it to show these after each tactic invocation?

(typing Show. works fine, but it's a nuisance to do it for each tactic)

This is coq 8.7.2, using coqtop

Thanks

Jeremy

[Coq-Club] displaying goal and hypotheses, Jeremy Dawson, 11/15/2018
- Re: [Coq-Club] displaying goal and hypotheses, Pierre Courtieu, 11/15/2018
  - Re: [Coq-Club] displaying goal and hypotheses, Jeremy Dawson, 11/15/2018
- Re: [Coq-Club] displaying goal and hypotheses, Enrico Tassi, 11/15/2018