aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ltac.out
blob: 20e274e2547401c33c11cc7ffe2715d4123277d2 (plain)
1
2
3
4
5
The command has indeed failed with message:
Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
Ltac f x y z :=
  symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
   dependent z