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: Jim Fehrle <jim.fehrle AT gmail.com>
Cc: coq-club AT inria.fr, Jason Gross <jasongross9 AT gmail.com>, Tej Chajed <tchajed AT mit.edu>
Subject: Re: [Coq-Club] help calling ltac1 function from ltac2
Date: Sun, 16 Aug 2020 19:09:35 -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-f176.google.com
Ironport-phdr: 9a23:4BADaRGblBJzxrkYVj4yz51GYnF86YWxBRYc798ds5kLTJ7yosSwAkXT6L1XgUPTWs2DsrQY0rSQ6vi6EjVQqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmssAndqtcajYR/Jqsy1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2zcpEPAvIPM+hYsYfzulgAohmwBQerC+zg1jBGi2Tq3aA4yektDRvL0BA+E98IrX/arM/1NKAXUe2twqXIzzLDb/VX2Tf+9ofIdg4uru+XULJ/dMre00gvFwffglqMrozlOj2Z3fkKvmiZ6OpgU+Ovi205pAF1vDeg2NwhiobMho0Py1DE8T91z5oyJd29UUN2Z8OvH5RMuS+ALYR2Xt8iTH9yuCY80rAKpZG2cDUXxJk5xxPSaP+KfoeW7xztW+ufLzl1iXx7dL+xhxu/7FWtxO3yW8WpzltEoDRIn9rCuH0J1xLd6suKR/1g9UmiwTaCzx7f5v1ALEwulqfWK4QtzqAumpYNq0jPAy37lUTugKOId0go5vWk5uH6brjiupCRMoB5hwDiPqgyn8GzHPo0MgYLUmeB5euzyKPv8Ej3QLpRgP02nKzUsJ7EKskauqG0Bg1Y3pgt5hmlCTqtzc4WkmMdLF1ffRKKl4jpNE/KIPD/Ffq/hk6jkDZvx/zfJ73hAYjBImHNkLv8f7tw6lRQyAU0zdBY6JJUDq8OLOjvVU/2sdzUFh45MwqqzOb7ENhxyJ8SVGaVDqKaMK7eq0GE6vwxL+WWeYMYujfwJ+Ag5/H0jH85nVEdfbOu3ZsScH24HPNmI0OYYXrvnNgBFXkFsRQlQezljV2NSz9TZ3KoU60g4TE7DZqqDZ3fSYC1nLyBwCC7E4VKaWBBE1CACGvnd4GZW/gXcy+SOc9gkjkcVbe7UYMh1BeutBX7y7V9NObU9DcY5trf041X5uibuxwy7zh5R5Cf0mTLQWx0hGcFbzAz1aF750d6zwHQ/7J/hqkSF9tV5vBEVgo3HZHZxu1+Tdv1X0iJKtWOTlelT9GrDBk+S9swx5kFZEMrSIbqtQzKwyf/W+xdrLeMHpFht/uEhyGsdfY48G7P0ewat3djQsZLMjf41Kt29gyWHo2Q1kvAyPjseqMb0yrAsmyEyDjW5RAKYEtLSazAGEsnSA7TpNX96FnFSub3W7siOwpFj8WFL/kTM4G7vRB9XP7mfe/mTSepgW7pXESHw7qNaMzhfGBPhCg=

On Sun, 16 Aug 2020 14:54:44 -0700
Jim Fehrle <jim.fehrle AT gmail.com> wrote:

> Maybe it would be good to collect more of these workarounds in a
> well-known place. I'm adding a few very short ones that @JasonGross
> suggested into the documentation, but this is a bit long to add
> there. Perhaps the wiki is the best place to do that? The doc could
> include a link to the wiki page. Hopefully these workarounds won't
> be needed in near future (say, by the 8.13 or 8.14 release).

At this point, the discussed hypotheses iterator doesn't contain
anything I'd label a workaround. But I think it is a very useful
example to document somewhere. Perhaps the wiki should have an Ltac2
Pearls page?

[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