test-suite/output/ltac_extra_args.v


1
2
3
4
5
6
7
8
9
10

Ltac foo := idtac.
Ltac bar H := idtac.

Goal True.
Proof.
  Fail foo H.
  Fail foo H H'.
  Fail bar H H'.
  Fail bar H H' H''.
Abort.