coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] navigating to bullets/braces
Date: Sun, 13 Jan 2019 23:50:06 +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-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:vTplqx/XeQ8off9uRHKM819IXTAuvvDOBiVQ1KB31eIcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZis1sg6xUrx2svAB/zJXObY2JKPZyYqHQcNUHTmRBRMZRUClBD5u4YYQRFeoOI+NYrongrFUAtxS/CxKsBOTpyjRVgXL42bM10/4/HgHD3A0sBdwAv27ardXuM6cSV/u4w7POzTXedf9Zxyry6JXSfh87vPGBRLR9etfSx0k3Dw7IgUmcpZb4Mz+J1OkBqXWX4uRhWO61j2Mqqxl9riWvy8swkIXFmJ4Zx17e+Sln3Yo5Oce0RFN1bNOgCJdQuT+VOohqTs4nRmxluTo2x78GtJO+eCUKxpAqyhDaZvGDboSH/w7vWeOPLjhjmH1ldrSyjAuo/0e60O3zTMy03U5KriVbltnMsWgA2gDd5caaVvdx416t1zGA2QzO8+1EJls7mrTBJ54m374wioEcsUPeHi/whUr6lreWdl8j+ui09evofqnmpp6bN49ykA3+NbkumtC7AeQ/NQgOXHKX9vi71L3m5UH5QbNKgeMqkqTBv53WOd4XqrOlDwJXyIov9hiyAja83NkcnXQLNFdFdwiGj4jtNVHOOvf4DfKnjlqojjhr3e7JPrjhA5nXIHbMirngfa16605a0wc819Zf549OBr4fPf3zR1X9u8bFDhMhKQy73/7nCMlh1oMZQW+AHqiZMLrLvVCU4uIvPvKDaZQOuDf9Lvgl/+ThgWU4mV8bZ6mp3IEYZGq2HvR8cA2lZi+midAYVGwOowAWTerwiVTEXyQZLyK5WLt57TUmAqqnC53CT8ajmurS8j28G8h0a3pLD0HEPX73bIKCE6MuZTifJ94nvjUbTr+nY4YnyFejuBK8wqcxfbmcwTERqZ+2jIs93ObUjxxnrWUlXfTY6HmESiRPpk1NQjY32K5lpkkkkAWK17U+jvBFU9VOtaoQDlUKcKXExuk/MOjcHxrbd47TGl+gX5OrDSx3R89jm4ZTMXY4IM2ri1X45wTvA7IRkODUVrUJyfqFml3cfoN6wXuA07Q9hV47RMcJLXehmqN06wnUAcjOjlmdkKGpM68b2XyU+Q==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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