I'd like to apply the same ltac_expr to multiple match_patterns in the Ltac language. For instance, I would like to do something like
match goal with
| H : context[true] |- _
| H : context[false] |- _ => my_tactic
end
as in OCaml, which is a syntax error in Ltac.
Thanks!
let
bind a tactic that you apply in both branches? $\endgroup$