0
$\begingroup$

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!

$\endgroup$
3
  • $\begingroup$ The documentation you point to does not seem to have such a feature? I are you hoping to use an undocumented hack? $\endgroup$ Commented Aug 5 at 2:17
  • 1
    $\begingroup$ @AndrejBauer I wasn't necessarily hoping to use a hack---I was curious if there was some Ltac-fu practiced by Coq wizards to match against multiple patterns :) $\endgroup$
    – Jay Lee
    Commented Aug 5 at 15:16
  • 2
    $\begingroup$ I guess you can just let bind a tactic that you apply in both branches? $\endgroup$ Commented Aug 5 at 20:45

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.