Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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
>



Archive powered by MHonArc 2.6.18.

Top of Page