coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] navigating to bullets/braces
Date: Mon, 14 Jan 2019 12:17:45 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:+Np7WhSOVl+Sz4wpQ9DQxRCXrdpsv+yvbD5Q0YIujvd0So/mwa6yYxCN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6bO/Vxc7jBfdwBX2dNQtpdWzBDD466coABD/ABPeFdr4Tlo1UBswG+ChepBOLv1zRGiGX53KMh0+QmFwHNwQstEdYQv3TOstr1MacTXfq7wqbSwzTDdPRW2THm5YfSdBAhvOuAUqxtfsrM00UgDR7Fg0yWpIf4PD2VzvwAvmeH4+Z6SO6jl2wqpxtsrjWhxMogkJTFip4Lxlzc+ih0xJw5KcC8RUN7e9KoDZRduiGAO4drQ84uXnlkuCgkxbAFpZK2eS0HxZU7yxPda/GKdoyF4hznWeufJDp1gG9pd6+jixu370ev0fHzVsey3V1XtCRKiMPMuWoI1xHL6siIVP99/kC51DuT2Q/d9/1ILV0tmaTGKZEszKc8lp0IvkvdBCP2n1j2jLONeUUj5+io7fnobq/+pp+GMI90lh/xPbgymsy+BuQ4NBICX2+G+eSg0L3j+kr5QLZQgvIqlanZtYjWJcUdpqGnHw9Yyoku5wqlAzu7zNgVn2MLIE9LdR+FlYTlJk3CLO7gAfe6mVuskTNrx/7cPr3mB5XANnzNn6n7fblj7k5dyBA/w95F6JNaEbEBJ/TzV1Tru9zeEx81KRK7zPv6CNlnzIweRHqDArWFP6PKrV+I+uUvLvGQa48SoTbxMuQq5/rzjXAiglIdZqmo3Z4PaH+iBPhmIkOZYWDtgtgbC2sKsBA+H6TWjwjIWjlKIn22QqgU5zchCYvgA52JDtSmh6XE1yOmFLVXYHpHAxaCCyG7WZ+DXqIuZTifJ94pvjUbTr+nA9sD2AujsR6857N4Ne3S0iQeqNTu2MUz7vCFxkJ6ziB9E8nIizLFdGpzhG5dH2ZnjpA6mlR0zxK46YY9hvVZEdJJ4PYQCFUzM4OawuBnTdnvCFuYIoW5DW2+S9DjOgkfC8oryoZUMU97BpOvgg2F1jf4W+ZIxYzOP4Q99+fn51a0J8t5zCqZhoActAF/B/B+biihjKM58BXPDYnUlUnfj7ytaakXwC/K8iGE0HaKu0ZbFgV3VPecUA==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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