coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] how to call ltac2 thunks from ltac1?
- Date: Tue, 18 Aug 2020 13:37:53 -0400
- Authentication-results: mail2-smtp-roc.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-f169.google.com
- Ironport-phdr: 9a23:Cv3iwBXksrljDhgtprYOlZZ+D6rV8LGtZVwlr6E/grcLSJyIuqrYbRWHt8tkgFKBZ4jH8fUM07OQ7/m+HzVYv93Q7DgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrAjdrNQajZdjJ6o+zhbErWZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJxw4DafpybOvl5cKzSYdwUSnFMXtpTWiFbHo+xdZcDA/QHMO1Fr4f9vVwOrR6mCAWiBuPvzTlIhn713aIk1+QuDx/J0RcvH9ILqnvUrdH1OL0OXuCyyanEwyjIYvRU2Tf67ojIcxMhru+IXb1ub8Xc0kYvFwbfgVWRrYzpJS+a1uMIs2WC6edrSO2ghXI9pQ5rvjiv2tkjipPPho8N11zJ9SV3zYkrKNGkVEN2YdypHZVMuiyVK4d7Qt4uTW90tCs+y7AIuZ22cTYWxJk72hPTdf6KfpSV7x/tVOufLzF1j29mdrKnnxu+71Ssx+nmWsS30FtGtDRJnsfSunwXyhDe68yKRuNj8kqgxTqDygXe5vxALE8okKfWJJ8szqIsmpcWvknOESH7lUTzgaOIeUgp/van5uH8bbn4qJ+cOYp5ig/gPasym8GyBOY1PRUTUGeB/+m3yaft8lfjQLpQi/07iqnZv47eJcQcvqO5BhVa0ocn6xqmFjem08kUkWAJLF5YeR+Ki5LlO17JIPD/Ave/h0qjnC13yPDBO73tGpTNLn7dn7f9Zbtx9VJQxQ4pwd1c559YEK8NLOztVkPrqdDVDxs0PxSxw+n9CdV90o0eWXiIAq+cKK7Ss1iI5uQuI+mPeoAVvCjyJOY+6v7hiH82g14dfa2z0ZQLb3C4G+xqI1+Fbnr0ntcBDWAKsxIiQ+ztkV2OSCJcZ3KvX60n/Tw7E4KnDYLbRo+3mrCB3SG7HodXZm9cEFyMH23oJM24XKIHbzvXKct8mHRQXr+4DoQlyBuGtQngyrMhIPCCqQMCspe2ntpy4ezQmBU/+BR7Cs2c1yeGSGQ+1jcKQDk33617rEFVxVKK0Kw+iPtdQ48Ar8hVWxs3YMaPh9dxDMr/D1qYI4W5DW2+S9DjOgkfC9I8x9hUPRR4EtSmywnAhm+kWuFE0bOMA5Mw/+TX2H2jf58smUaD77EoihwdeuUKMGSngqBl8A2KXtzGlkyYk+ChcqFOhXeRplfG9nKHuQRjaCA1Sb/MBClNaU7frNC/7UTHHeej
I have a let-defined Ltac2 thunk of type unit -> unit. How do I pass
it to an Ltac1 tactic so that the Ltac1 tactic can execute the Ltac2
thunk? It seems that I have to convert the thunk to type Ltac1.t
somehow in order to get it across the Ltac1/Ltac2 interface, but I don't
see how to accomplish that.
- [Coq-Club] how to call ltac2 thunks from ltac1?, jonikelee AT gmail.com, 08/18/2020
Archive powered by MHonArc 2.6.19+.