I would like to understand how to use the Ltac2
unfold tactic inside an Ltac2 function.
I know that, when proving a goal, we can use
lemma_name is the name of a previously proven lemma, and the above tactic unfolds
lemma_name in the goal.
However, I would like to create a custom function that calls the Ltac2
unfold tactic. The only way I have managed to do it is as follows:
Ltac2 my_unfold (t: constr) := unfold &t
However, when calling the above function, it returns an error of the form
Anomaly found. I do not know how to call the Ltac2 unfold tactic otherwise (the purpose of the above function is to call more tactics/functions, not just the Ltac2 unfold).