coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] displaying goal and hypotheses

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] displaying goal and hypotheses
Date: Thu, 15 Nov 2018 11:35:48 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f41.google.com
Ironport-phdr: 9a23:C6/nix8MGvdmEP9uRHKM819IXTAuvvDOBiVQ1KB40e0cTK2v8tzYMVDF4r011RmVBdqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDmiCgFNzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMDJm9b4QRFeoBJ/hXpJTjqlsJsBu+HxWsBOLxxT9Vm3T72rU60+U/HgHcxgwvAcgCv2jTrNXoLqcSTeG1w7fVzTjYYPNW3C3y6InMchw7vf6MWrdwfNPXxEIyFA3Flk2dpZL5Mz6RzOgAsGiW4/B+We6yl2IrsQ58riWpy8wxkIfGnJgVxUrB9ShhwIY6O9m4SEljbN6hCpRQtiWaO5JxQsM+Xm1koSg6x7IbtZKhcygKz5MnxxHba/OZaYSH/hXjVOOJLTd5gnJqZq6/ig6s/US8zuDwTMq53VZQoiZbj9XAqmoB2hPO5sSfT/ty5Eah2TKB1wDJ7eFEJFg5lbLaK5E/2L4wjIQcvV7fES/xhUX2lrOWdkQ69ei18OnnbbDmqYWdN49wkA3xLqMumsmnDeQiLgcOR3Sb+fi71LD74UL5R6xKguQqnandrZDVPt8WprW5Ag9QyoYs8QyzDzag0NQCnHkINkhJeBydj9uhB1abK/fhSPy7nl6EkTFxxvmAMKeyLI/KKy37kbr7Z7s1wElB0hYywM0Xs4pVB6sbLbT4XVLrqN3VEzc2NgW1x6DsD9ArhdBWYn6GHqLMaPCailSP/O96e7DdNr9Qgy70Lr0e39CriHY4nVEHeqzwhMkYbXm5GrJtJEDLOCOw0OdEKn8Du08FdMKvkEeLCGcBaHO7XqZ67TY+Wtr/UNXzA7u1ibnE5x+VW51bYmccVwKJGHbsMoKYArICNHvULchmnTgJE7OmTt152A==

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> 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