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 constr
s is the best I could come up with
Last updated: Oct 13 2024 at 01:02 UTC