Is there any way to force evaluation of an ltac2 term at definition time of a tactic to get around the
Tactic definition must be a syntactical value error? I have a tactic that uses ltac2 to work around ltac1 insufficiencies (taking a list of hint dabases, to be specific) but the workaround is slow (since it parses coq strings into ltac2 idents). This would be fine if I could evaluate the workaround once and stick that into its own tactic but I don't know if there is any way to do that.
Just to elaborate a bit: eventually all of this needs to be called from ltac1 so a ltac1 tactic notation taking a list of
constrs is the best I could come up with
Last updated: Sep 26 2023 at 12:02 UTC