I am sorry if my question is trivial, but how and is it possible to write a tactic which allows to iter on all hypothesis in the context, and apply a certain function (constr or ltac on it). I struggle with the 'match context' I think.
Put your action next to
change, then you can do
Ltac foo := match goal with | H: ?P |- _ => lazymatch P with | id _ => fail | _ => change P with (id P) in H end end.
Thank you for your help !
Last updated: Jan 31 2023 at 12:01 UTC