coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] help calling ltac1 function from ltac2

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: Jim Fehrle <jim.fehrle AT gmail.com>, coq-club <coq-club AT inria.fr>, Tej Chajed <tchajed AT mit.edu>
Subject: Re: [Coq-Club] help calling ltac1 function from ltac2
Date: Tue, 18 Aug 2020 11:59:17 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f171.google.com
Ironport-phdr: 9a23:8MZERhAKLR8XYtiJJIuUUyQJP3N1i/DPJgcQr6AfoPdwSP37p8ywAkXT6L1XgUPTWs2DsrQY0rSQ6vi+EjNbqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmssAndqsgbjYRgJ6s/1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2zcpEPAvIPM+hYsYfzulgAohmwBQerC+zg1jBGi2Tq3aA4yektDRvL0BA+E98IrX/arM/1NKAXUe2twqXIzzLDb/VX2Tf+9ofIdg4uru+XULJ/dMre00gvFwffglqMrozlOj2Z3fkKvmiZ6OpgU+Ovi205pAF1vDeg2NwhiobMho0Py1DE8T91z5oyJd29UUN2Z8OvH5RMuS+ALYR2Xt8iTH9yuCY80rALu4K2cigXxZkoyRDTdvOJfYaG7x/+W+ucPTh2iXZ4dL+wmRu+7Emtx/PzWMe03ltEoShInNbMuH4C1xLe9tWLR/1g9Umv3jaP0hrc6uBCIU0smqrbKoIhwr4tlpUIq0jMAij2mEDwgaSLdUsk4vCl5/r7brjivJORNI95hhvgPqgwhMCzG/k0PwoTU2SD5+ix1aHv8VD8TblXivA5jqzUvZ/bKMgHuqK0BgBY34kt5hu+CjqqztsVkH0ZI19AYx2LkYbpO1/LLfD2E/iwn1WhnTJpyv/bI7LuGJPAJWXZnrj7Z7Zy8UtcxRIzzd9B45JUDakMIPfpVU/wsNzUFwY5Mw+pz+r+BtVxy4ETVX+VDq+WN6PStlCI5uYxLOWWeIAVvzP9J+Ak5/7ok3A5hUcQcbe10ZYTcny1HfRrL1+HbXbynNsNC3oGswgjQODyjV2NSz9TZ3K8X6Im4TE7DZqrDYXERoCrgbyB3zm0HplIaW9YEV2MHnLoeJ+FW/cIci6dPshhkjkcWbi7V4AhzQ2utBP9y7d/MuXU/TQYuYv/29hx+u3cjgo/9Sd0DsSYy2GCVXt4nmIORz8s3aBwu1ZxylmZ0fswv/sNN9VI4PUBfR09LoWUm+5zENf0VRjGZczYYFmjS9SiRzo2S4Ri7cUJZhM3GdKkjxPO2yenK7AQnr2PQpcz9+iUi3r2Icd+xnLL2YEuilAnRo1EMmjw1f03zBTaG4OcyxbRrK2tb6lJmXeVrD7en1rLh1lRVUtLaYuAXX0bYRGI/9Hw50eHVrz3TLp+bVIHxsmFJa9HLNbuiAceHauxCJHle2u03lyIK1OQ3LrVNdjlfmwc2GPWD01Wy1lCr0bDDhA3A2Kam0ybCTVvEVz1ZEa1qLtxrXq6Sgk/yATYNkA=

Thanks. I added it to https://github.com/coq/coq/wiki/LtacPearls

On Mon, 17 Aug 2020 22:51:59 -0400
Jason Gross <jasongross9 AT gmail.com> wrote:

> Possibly https://github.com/coq/coq/wiki/OtherContents or
> https://github.com/coq/coq/wiki/LtacPearls (or start an Ltac2Pearls
> page and update the link on
> https://github.com/coq/coq/wiki/OtherContents to distinguish between
> Ltac and Ltac2, rather than just having "Tactic pearls"). Note that
> the first of these is linked as "More content" on
> https://github.com/coq/coq/wiki#coq-wiki
>
> On Mon, Aug 17, 2020 at 8:54 PM jonikelee AT gmail.com
> <jonikelee AT gmail.com> wrote:
>
> > I created a rather longish gist about Ltac and Ltac2 hypothesis
> > iterators that incorporates what was discussed in this thread:
> >
> > https://gist.github.com/jonleivent/62e1925b8702db9a0677ea02d4cf6cd3
> >
> > Where is the appropriate place to link this in Coq land?
> >

[Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/16/2020
- Re: [Coq-Club] help calling ltac1 function from ltac2, Tej Chajed, 08/16/2020
  - Re: [Coq-Club] help calling ltac1 function from ltac2, Jim Fehrle, 08/16/2020
  - Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/16/2020
    - Re: [Coq-Club] help calling ltac1 function from ltac2, Jason Gross, 08/16/2020
      - Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/16/2020
        
        Re: [Coq-Club] help calling ltac1 function from ltac2, Jim Fehrle, 08/16/2020
        
        Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/17/2020
        
        Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/18/2020
        Re: [Coq-Club] help calling ltac1 function from ltac2, Jason Gross, 08/18/2020
        Re: [Coq-Club] help calling ltac1 function from ltac2, jonikelee AT gmail.com, 08/18/2020