coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] navigating to bullets/braces

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] navigating to bullets/braces
Date: Mon, 14 Jan 2019 13:26:10 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk1-f177.google.com
Ironport-phdr: 9a23:MZjNRRWR7K7PqzqYffOofvF30LjV8LGtZVwlr6E/grcLSJyIuqrYYxKHt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZDYy8YYkAAeoPM+hbsofzuUcBoACkCgWwHu7i0CNEimP00KA8zu8vERvG3AslH98WrnrUrM/yNKAKXu+2zanIyDDDYO1M2Tf48ofIdBYhquyLULJsccre104vGxnEj1WRrIzlOjKV2/8Cs2ie9eVgVOavh3Q7pAF2pzii38EhgZTKiIIN0l3I6zl1zYIvKdC7SEN3e8CoHIVNuy2AKod7QMEvTmd1sygg0LIGo4S0fC0SxZQn2RHfb/uHfpCN4h35VeaRJS50hGxmeL6inhqy/1Wsx+/+W8Wu31ZKqS1FktbItn8TzRDc9s+HSv5l8keg3zaAyRzT5/laLUwokafXMZ0sz74qmpYNr0jPAzX6lFj0gaKUbkkk//Kn6+XjYrXovJ+cMIp0hxniMqQuhMO/Bv40MwkPX2ie/OS81abu/UL8QLpQj/02lrPVv4zdJcQevqK5GRNa0p4/6xajCDeryMgXnX4eLF5cZB2Hi5XpNErVLfDjDfa/hkysny1xy/DHOL3hGJTNIWLZnLfvZ7Yuo3JbnSE01Jh0449eQuUKJ+u2UUvsvvTZCAU4Okq62bC0Js9609YiWeOINZ2YNabfq1qB4ORnd/WMaYhTqjf4LvkN6PvnjHt/klgYK/r6laALYWy1S6w1a36SZmDh15JYST9T71gOCdfygVjHagZ9InO7XqYy/DY+Udv0AoLKR4Tri7uEjn7iQs9mI1teA1XJKk/GMp2eUq5VOi2XK85l1DcDUOr5EtJz5VSVrAb/joFfAK/U9ykf78yx0dF046jNlkh3+2UrUIKS1GaCS2wylWQNFWc7

coqtop is not really getting many new features these days, as it is considered to be only used for debugging... and not really recommended for actual proving...

Cheers,

Théo

Le lun. 14 janv. 2019 à 13:18, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :

Hi Theo,

Yes, it would also be a good feature for coqtop

Cheers,

Jeremy

On 01/14/2019 09:19 PM, Théo Zimmermann wrote:
> Hi Jeremy,
>
> To my knowledge, there isn't currently such a feature. This seems like a
> good feature-request for user-interfaces such as Proof-General or CoqIDE...
>
> Théo
>
> Le lun. 14 janv. 2019 à 00:50, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au
> <mailto:Jeremy.Dawson AT anu.edu.au>> a écrit :
>
>
> Hi,
>
> is there a way of Undo-ing a current proof back to the previous
> occurrence of a given bullet, or to the previous occurrence of { ?
>
> Thanks
>
> Jeremy
>

[Coq-Club] navigating to bullets/braces, Jeremy Dawson, 01/14/2019
- Re: [Coq-Club] navigating to bullets/braces, Théo Zimmermann, 01/14/2019
  - Re: [Coq-Club] navigating to bullets/braces, Jeremy Dawson, 01/14/2019
    - Re: [Coq-Club] navigating to bullets/braces, Théo Zimmermann, 01/14/2019
      - Re: [Coq-Club] navigating to bullets/braces, Jeremy Dawson, 01/14/2019
        
        Re: [Coq-Club] navigating to bullets/braces, Laurent Thery, 01/14/2019
        
        Re: [Coq-Club] navigating to bullets/braces, Jeremy Dawson, 01/15/2019
        
        Re: [Coq-Club] navigating to bullets/braces, Théo Zimmermann, 01/15/2019
        Re: [Coq-Club] navigating to bullets/braces, Laurent Thery, 01/15/2019
        
        Re: [Coq-Club] navigating to bullets/braces, Jeremy Dawson, 01/16/2019