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
|
