coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] help calling ltac1 function from ltac2
Date: Sat, 15 Aug 2020 21:05:11 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f45.google.com
Ironport-phdr: 9a23:oVJ6UhHpvux4GDBDVe2Ijp1GYnF86YWxBRYc798ds5kLTJ78r8uwAkXT6L1XgUPTWs2DsrQY0rSQ6vi4EjNfqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmssAndqtUajYRgJ6sz1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrx2vpxN9w4DaboKbOudgcKzBZt4VX3ZNU9xLWiBdHo+xbY0CBPcBM+ZCqIn9okMDox+/BQmpGejhyiFHhn/s3a0+zesqDAbL3A4hH9ILqnjUosv6NKcIUeCx0qbF1jrDb/ZM1jf87IjEaAwuofaJXb9pd8fa1EYgGR/fgFqKtYzlIy2a1v4Ls2WD8+dtVvyihmoopgxwpjWixNsgh5fHiI8R1lzJ6SF0zJo0KNC2SUN2f8CpHIdUuiyeNYZ7Tc0sTnxntisn1LAKpZi2dzUJxpQ/3xPTdeCLfoyS7h/gVOudOyp0iXNkdb6liBu/8U6twfDmWMauylZFtC9Fn8HMtn8T0xzT7dCKSv5n8Ueg3TaDzgHT6uZZLUwtm6rWJJ4szqQ/lpoUtkTDESv2l1vsgKCKcUUk//Ck6+XhYrr4up+RL5F4hh36P6g0mcGyAf40PhUPUmWa4+ix273u8VX8QLpQj/02lqfZsIrdJcQevqO5AQ5V0oM55xaxETim0M4YnX0ZI19edxKHipLmO1DKIPziEfi/hFGsnC9xx//aJr3hHonNLn/bnbj9erZ98ldQxxY3zdBC/J1ZEaoBIfL2Wk/prtPUFB45Mwquw+bmEtpxzI0eWXjcSpOeZajVqBqD4v8lC+iKfo4c/jjneNY/4Pu7r3480XEQfbOt0NNDanG9WPprI1+dbFLjh94AFSEBuQ9oH7+is0GLTTMGPyX6ZKk7/DxuUNv6X7eGfZikhfm65An+BodfPzkUBVWFEHOufIKBCa9VNXCiZ/R5mzlBboCPDo8s0Rb06V3/wrtja+vTo2gW6c+l299y6One0xo18G4sVpXP4yS2V2hx21gwaXoz1aF7r1Z6zw7ag6d9iv1cU9dU4qEQXw==

> please complain to Pierre-Marie

Please file an issue and cc to @ppedrot or indicate your support for an existing issue.

[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