coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] navigating to bullets/braces, Jeremy Dawson, 01/15/2019
- Re: [Coq-Club] navigating to bullets/braces, Laurent Thery, 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, Théo Zimmermann, 01/14/2019
Archive powered by MHonArc 2.6.18.