Dear community,

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

`unfold lemma_name`

where `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).