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 21:14:01 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.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:AfqHlxAiCmwcDn2jVgGqUyQJP3N1i/DPJgcQr6AfoPdwSPT8o8bcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzLisJ+j6xbrhCupx1jzIDbb46YL+Z+cbjHcN8GWWZNQsRcWipcCY28dYsPCO8BMP5coYbjvVsBsx6+BAmxD+3h0DBJiGT23ao80+88FgzI2BIvH8gQv3TRrNT5LqkcXvq7zanTyjXDaehb1i376IjVaBwuv+yDXa9qfcXL1EkiDgXIhUiTp4z9Jz6Y2fgBv3KG4+Z8V++jkXMrpg9zrzS128sglo3Eipoax13A7yl13YI4KN2iREJmbtOpEIFcuzybOodrWs8iTX9ntSUmxrADvJO2fTQGxZYnyhPab/GHfYyF7xzmWeuVPDt3mW5pdbehiBmp7UegxOvxXdSu3llQtCpKiNzMu2gN1xPN7siHTeNw81uv1jiSywzf9/hIL102mqfVMpIhxaU/mYQJvUTEAy/2hF75jKiLdkUi5+ek8fznYq/hpp+AKYB7lh3+MqUpmsy5G+g4NRUOX3Sf+eS7073j/lf1T6lNjv0ziqXZsZbaKtoHpqOhDAJZzpwv5wujAzqkytgUgHcKIVBfdB6ak4TkP0nCIPXiAve+h1Ssni1rx/fDPrD5BpvCMGLDn6nkfbd98UJSxhA8zN5E55JTDLEMO+j8WknstNDCEBA2LhG0z/z9B9Vgzo8eQ36AAreFMKPOtl+F/v4gI+6VZIMMpDn9L+Ul6OX1gH8imV4deLGp0oENZHC5GPRmOUSZbmD2jtcPC2dZ9jY5Gabhj0THWjpObV6zWbg973c1EsjuWYzEX8WmhKGL9Ca9BJxfIG5cXAOiC3DtIqeJQfoJeWq+K9B6lTpMAZqsUYIkxFeCvRDhzLxPJ+zJvCAUqNTqyY4mtKXoiRgu+GksXIym2GaXQjQsxzJad3oNxKl65HdF5BKG2Kl8jeZfEIUJtfpPT0E3OYOaxvEoUomuCDKERc+ATROdevvjGSs4F4hjytkTJUtxBpOrk0Kbhnf4M/ouj7WOQacM3Ofc0nz2e5kv4kv9jPBktGh9B8xFOCuhm7J18BXVC8jRiUKFmq22dKMaminQ6GOEymnIt0ZdAld9
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Well, how do I run coqide? The doc says CoqIDE is run by typing the
command coqide on the command line. but my system has no such command.

I'm using the Fedora package coq. Is there a different package for coqide?

Thanks

Jeremy

On 01/14/2019 11:26 PM, Théo Zimmermann wrote:
> 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
>
> <mailto: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>
> >
> <mailto: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