aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Tactics.out
blob: 9949658c44c47f6e91abffd26f35e6f4094471e2 (plain)
1
2
3
4
Ltac f H := split; [ a H | e H ]
Ltac g := match goal with
          | |- context [if ?X then _ else _] => case X
          end