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: Mon, 17 Aug 2020 20:54:01 -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-f172.google.com
Ironport-phdr: 9a23:ZGCGPhA/pzRXVMpLIiPBUyQJP3N1i/DPJgcQr6AfoPdwSPXyocbcNUDSrc9gkEXOFd2Cra4d1ayP6/2rAjJIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLJ/IA+roQnNtsQajoVvJ6cswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKLCAy/n3JhcNsjaJbuBOhqAJ5w47Ie4GeKf5ycrrAcd8GWWZNW8BcXDFDDIyhdYsCF+QPM+ZGoYfgpFUBrxW+Cw6jC+zzxTFFnWP20K803ug9CwzKwBIsEtQTu3rUttX1M6ISXPi7wKnKyjXDafJW2TTj54jMbB8uv+qBXb11ccXLyEkvExnJgUmXqYzgMT+ey+MAs2qc7+pmVOKviHAoqwVvrTex3coshYzJiZgUylDA7yl23IE1JdihRUN9fNWrH4deuTuAOItqXsMtXXtouCAix7AEp5O2YScExYomyhDfdvGKcpWF7wzsWeieLzl1hX1rdbO7ihux7EWuyuzxW9S73VtIoSRJjt3Bu3AO2hLd5caKTOZ28Emm2TaKzQ/T6+dELFg7laraN54hwqMwmYEJvUvfGS/2nUP7h7KVeEU84uWk9fjrb7H8qpKfN4J4kB/yProwlsClHOg1MBYCU3CF9em9yLHv4Ej0TKhOg/Iql6TUv5HXKdgHqqO8DAJY3Ygu5he6Aji839kXgXYKIVdLeB6agYjpNVTDIP7mAvujnlihlS1kyO7GM7DnH57DNGLMkK37crZ480NcyBQ8zdRY559MD7EOOvPzWkvouNzBDR81LhW4w+j6BNh/yI8SQ22PAqieMKPdtV+H+PgjLPWLZI8QoDr9Kv4l6ODyjXIhh1MRYa2k0YEUZX24BPhqPVuVbWT2jtscE2oGoBIyTOnwh12DVT5TaWyyX6U55jwjCoKmCoHDRoGugLOf2Ce0AINZa3tJClCJC3jodoGEV+0QZyKVJ89tiiYEWqS5S489yRGusxf3xKZgLurN4yEXqZbj1MVu6ODIjhEz9Tl0D9yH3G2XTmF0mHkIRz4s06xlr0x90ATL7a8tof1dXfJe5+lNX09uN5/ZieJ3C8r2VyrOe96ITBCtRdDwUh8rSddkid0JZUd+FtGvgzjM2iOrB/kekLnBTMg29aTd3HX1KstVxHPP1a1nhF4jFJgcfVa6j7JyolCAT7XClF+UwuPzLfxFjXz9sVybxG/Lh3l2FQt5UKHLR3caPxKEotHw50eERLirW+1+bllxjPWaI64PUeXHyE1cTa66atvbamO13Wy3AETQn+7eXM/RY2wYmR7lJg0EngQUpyjUMAE/AmK4oDubAmUxTxTgZETj9eQ4o3S+HBc5

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