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
Cc: 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 14:54:44 -0700
Authentication-results: mail3-smtp-sop.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-f54.google.com
Ironport-phdr: 9a23:7BGdnBTHUI5nEbjO30gFxNNmZNpsv+yvbD5Q0YIujvd0So/mwa6yZhyN2/xhgRfzUJnB7Loc0qyK6v6mADRaqs7a+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi3oAnLq8UanZVuJqktxhbHv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/XrJgcJskq1UvBOhpwR+w4HKZoGVKOF+db7Zcd8DWGZNQtpdWylHD4ihbYUAEvABMP5XoInzpVQArRWwCwqxCu3x1jBFnWX50bEg3uk7DQ3KwA4tEtQTu3rUttX1M6ISXPixwqnJyDXIcvNY1in96IjSdhAuv+yHULVyccrQzEkjDQ3FgUuQqYz/OzOayP8As2ee7+V6VOKvj3QrpB12ojiq38ohjJTCiY0JxF7e7yp53Jo1KsOiSE59edOpDJhduj+eOoZ5Q84vR2NltDokx7MIvZO3YDQHxZA7yxPeZfGKcpaF7wz/WOuVJTp1hn1odryiihi97EWt1PHwW8+p21hJtipIisfAumwJ2hDJ6cWKSuFx8lqg1DuOzQze6u5JLEYpnqTBMZEh2KQ/lp8LvETDACD2nEL2gbeTdko+++io7/3rYrThppOBLoN0hAHzP6s0lsywBuQ4NQcOX2yF9uimyLLj+kj5TK1Ljv0wjKbZrIjXKdoHqqO9GQNY0YYu5wyiAzqn0dkUh3kKIV1ddBKClYfpOlXOIP7iDfe4hlShiDVrx/HDPrH7DJXCMHjDkK3lfblj8ENcxw8zwspe55JQEL0OPPXzWkrpuNzCEhA5KxC0w/rgCNhlyoweXnuPDraFP6PWrF+H/fkiI/KMZY8QoDbyMeIp5//ojX8jmF8SZ7Ol3ZUNaCPwIvMzKEKAJHHon90pEGEQvwN4Qva5pkeFVGtxZnP6ca88/DU2QNakDIKFSI2tmriM9Ci+F5xSIGtBDwbfQj/Ta4yYVqJUO2qpKch7n2lBDOD5EtNz5VSVrAb/joFfAK/M4CRB7MDs0dF046vYkhRgrWUlXfTY6HmESiRPpk1NQjY32K5lpkkkkwWM1KF5h7pTEtkBvqoUADd/DobVyqlBM/63Wg/FeY3UGlOvQ9HjADZoC9xsn5kBZEFyH9jkhRfGjXKn

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).

[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