coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [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>, Pierre Courtieu <pierre.courtieu AT gmail.com>
Subject: Re: [Coq-Club] displaying goal and hypotheses
Date: Thu, 15 Nov 2018 12:09:44 +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-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:+3huqRbNwxmSmQEw5Y8h4fr/LSx+4OfEezUN459isYplN5qZrsm8bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVyJPHJ6yb5cBAeQCM+ZXrYj9qEcBoxSxHgSsGPjgxyVUinPqwaE30eIsGhzG0gw6GNIOtWzZotHrO6cIT++1yanJxijNYfxM1zb984/IchY8qvyLWbx/b9DRxlcqFwLFlFmep5bqPj2O1uQKtWiW9PBvVeSyi2I9tQ5+vyWvyt02hYnUn48YzE3P+yZhwIstKtC0VFR3bcO4HJZSrS2WKoV7T8E4T211pSo3yaUKtJG/cSQQ1Zgqwx7SZ+aJfoWG+B7uUOScLS92hH17e7+zmxO//E2uyuLhWMS4zVNHoy5Ln9TOuHAA0gHc58qER/Rh+0quxCuA2B3P5exCPEs6j7DUK4Q7zb41jpcTsVrMHivxmEjukKKZeFgq9vS15+j+f7vppJGRO5Zzig7lLKsigMu/AfkkMgcVWGib5OK826D58U3hWrVKieE2nbfFv5DGJMQboai5DxVS0oY+9xa/CzCm0NMbnXUdMF1FfxeHg5DoO1HIPv/4Ee+yjluwnDtx2vzKIr/sDo/QInXNkrrtZ6tx51NfxQYryNBQ/ZNUCrUPIPLpXU/xscTVABsnPAyu3ennDdV82pkQV22VDK6ZK6TSsVmT6+01JemMeZUZtyjgJPg4/fLhl2I5lUcHfaa1xZsXdGy4HvN+LkqFZnrsm84NHnsOvgojV+Pnk0aCUD5WZ3aqRa0w/DA7CIS8DYfCXI+hmrKB3D3oVqFRMypNDUnJGnP1fa2FXe0NYWScOIUpxjcDTP2qT5Ir/RCorg7zjbR9eK6cwiwVr4junPNy+vfPlBwvvWhsDsmHyWzLRGZphH8JSiIe06V2oEg7wVCGh/tWmftdQP5e/f5MQ08WPIHHyOoyX/L/QA/Eb5GlQUm9RdOOCDcsCN893pkHfhAuSJ2Zkhnf0n/yUPcunLuRCclxq/qEhimjF4NG03/DkZIZoRwjS8pLO3ehg/clpQHVGsjEn1jfnrv4LP1Ajh6Iz3+KyC+1hG8dSBR5CP+XVHYCIEbasJLw+xGaFuL8OfEcKgJEjPW6BO5KZ9nu0QoUbcrYYI2bWFPq3mC6CFCP26+Ga5fsdyMFxiLBBUMYkgcVu3GbKQw5ASTnqGXbXmVj
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi,

I just type coqtop (actually coqtop -color no) into a terminal window.

Sorry if I don't understand your question.

Cheers,

Jeremy

On 11/15/2018 09:35 PM, Pierre Courtieu wrote:
> Hi, It looks like a problem with the interface. Which one do you use?
> coqide, Proofgeneral, something else?
> Pierre
>
> Le jeu. 15 nov. 2018 à 09:35, Jeremy Dawson
> <Jeremy.Dawson AT anu.edu.au
>
> <mailto:Jeremy.Dawson AT anu.edu.au>>
> a écrit :
>
> 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