Is there any fundamental reason that
Ltac2 Set only works when I declare the original tactic as mutable?
If not, I propose that "is not declared as mutable" be a warning that is fatal by default (but can be made non-fatal). I find
Ltac foo ::= ... to be very useful for debugging and prototyping when I don't want to recompile all the dependencies, and would like to be able to do the same in Ltac2, even if this is strongly discouraged. (I'm even fine with this feature only working interactively and not being able to be persisted to .vo files, if need be.)
Last updated: Nov 29 2023 at 19:01 UTC