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 11:19:51 +0100
Authentication-results: mail2-smtp-roc.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-ua1-f43.google.com
Ironport-phdr: 9a23:s1GSkRS1YLcGRlpEBBghrBy6edpsv+yvbD5Q0YIujvd0So/mwa69YRCN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0ligIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNgHR2ROQ9xRWjRODYOybYQBD+QPM+VFoYfju1QDtgGxCRW2Ce711jNEmn370Ksn2OohCwHG2wkgEsoQvnTUttL1M78dXuO0zKnNyDXMcelW2TLn54jOdBAqvPaBXa5wccXPzkkjDQLEjlSVqYzgPjOYzesNs22B4OphUeKjkXIoqwZ0ojW2wMonl4rHhpoNx1za6Sl0xJw5KN64RUJhf9KoDoVcuzuVOoZ4RM4pXntmtzwgyrIcvJ62ZCgKx4ojxx7Yc/GHdpKH4hPnVOqIPDd3nm9pdKuxhxu9/0Ws0OL8Vs6z0FZFqipKjMPAuWwK1xzW8sSHS/198Vm92TuXyQzf9uVJLVo3mKfbMZIt3KA8moQJvUnMECL6gED2g7WXdkUg9Oio8ePnYrD+q5+AN497lAb+Pr4vm8y+BOQ4NwkOUnOU+eS5zrLj/En5TK9Wgf0xl6nVqIraKtgDpq6lHw9V1Z4u5Aq4Dze/ydgXgX0HLE9edx+clIjoO1TOIOjiAvulglSsli1rx/HcMbH7DJXNNCuLrLC0VrFko2VY1QB7mdtY/tdfDqwLCPP1QE748tLCWEwXKQuxltrnidJK5IIbXG+VB6afNuuGrV+F4aQ9IuyJZacavT/8L74u4Pu43ixxokMUYaT8hchfU3u/BPkzZhzBOSO90OdEKn8Du08FdMKvjVSDVTBJYHPrBvAz4zg6DMStCoKRH9nx0ozE5z+yG9htXk4DEkqFSC66eICNWvNKYyWXcJc4z240EIO5Qopk7imA8Q/3z709c7jR8ywc8I/qjZ17u7aVmhY1+jh5Sc+a1jPVQg==

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