File "./output/ltac.v", line 8, characters 13-31:
The command has indeed failed with message:
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
File "./output/ltac.v", line 38, characters 5-9:
The command has indeed failed with message:
The term "I" has type "True" while it is expected to have type "False".
In nested Ltac calls to "g1" and "refine (uconstr)", last call failed.
File "./output/ltac.v", line 39, characters 5-9:
The command has indeed failed with message:
The term "I" has type "True" while it is expected to have type "False".
In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call
failed.
File "./output/ltac.v", line 40, characters 5-9:
The command has indeed failed with message:
The term "I" has type "True" while it is expected to have type "False".
In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call
failed.
File "./output/ltac.v", line 41, characters 5-9:
The command has indeed failed with message:
The term "I" has type "True" while it is expected to have type "False".
In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call
failed.
File "./output/ltac.v", line 46, characters 5-8:
The command has indeed failed with message:
No primitive equality found.
In nested Ltac calls to "h" and "injection (destruction_arg)", last call
failed.
File "./output/ltac.v", line 48, characters 5-8:
The command has indeed failed with message:
No primitive equality found.
In nested Ltac calls to "h" and "injection (destruction_arg)", last call
failed.
Hx
nat
nat
0
0
Ltac foo :=
let x := intros in
let y := intros -> in
let v := constr:(nil) in
let w := () in
let z := 1 in
pose v
2 goals
n : nat
============================
(fix a (n0 : nat) : nat := match n0 with
| 0 => 0
| S n1 => a n1
end) n = n
goal 2 is:
forall a : nat, a = 0
[ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
]
