coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason Gross <jasongross9 AT gmail.com>
To: "jonikelee AT gmail.com" <jonikelee 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: Mon, 17 Aug 2020 22:51:59 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f50.google.com
Ironport-phdr: 9a23:Ui/hPx3YAQD2t1sasmDT+DRfVm0co7zxezQtwd8ZseMWKvad9pjvdHbS+e9qxAeQG9mCtbQd07ed7fiocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTuwbalvIBmqrQjducgbjZd/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTlkzkMOSIn/27Li8xwlKNbrwynpxxj2I7ffYWZOONjcq/BYd8WQGxMVdtTWSNcGIOxd4QAD+QDMuhYoYfzpEYAowWiCgS3Huzj1iVFi2Xq0aEm0eksFxzN0gw6H9IJtXTZtNH7O70JUeCyyqnD0DTNb+lR2Tfm84jDbxcsofOWUrJrdsrRz0YvFxnCjlWLsozoOyiY1usIs2eB7upgUfijhHIgqwF0uzWiwNonhYbViIwP0F/E6Tl5z5gvJd2+UEN2f9qpHpVMui2HNIZ4TM0vTn1mtis6xLALuIK2cSgUxJkj2RPRZfOJfomI7x/9SOqdPCp1iXJkdb+8iBu/7Fasx+vhXce611ZKqzBKktjKtn0V2BzT69SHSvtg/ki6wzqAywfT6uRCLEsplqTbM4YszqAsmpcXq0jOHS/7lF/ogKOLdUgo4Oil5/jhb777vJGTLZV0hRv7Mqk2msywH+A4Mg8WUmie4+u81bnj8VTnT7VIk/E6i6fZvZDGKcgBqa65BAhV0okn6xmhFTupzNMYnXwfIFJEfhKIkZTpNknQLPzkCfqzmVehnTdxy/zYI7HsAY/BI3jfnLv5eLZy8U9cyA49zdBF4JJUD6kMIPDpVU/qs9zYCBA5Mxazw+b8E9Vw0pgTWW2KAqCDMaPStUWE6f4oI+mJfIMVoiryK+A55/7yin80gUMSfa6w3ZcOdH+4GulmLF6CbHr3gtYBFH8KsRAkQOzrjl2CSz9TaGyoU6Iy/DFoQL6hWM3BQYasg7GF0SqTEZhfZ2QAAVeJWz+8dYKCWvQBbC+fCsBkmz0AE7OmTtly+wupsVrYwqFgKKL74CoDrtq31tFu4OvcjxYp7m1cAMGU0mXLRGZxyDBbDwQq1bxy9BQugmyI1rJ11rkBTYQKuqF5FzwiPJuZ9NRUTtD/XgWbI4WMQVeiB9ikWHQ/E4p3zNgJbEJwXd6li0Kbhnv4M/ouj7WOQacM3OfZ1nn1Kdx6zi+fhqYkhlgiBMBIMD//3/Itx03oH4fM1n6hueOyb61FhXzC8W6CySyFu0QKCAM=

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