blob: e30c97aac664410e03d00f57895fa22daa917508 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Set Ltac Backtrace.
Ltac foo x := idtac x.
Ltac bar x := fun y _ => idtac x y.
Ltac baz := foo.
Ltac qux := bar.
Ltac mydo tac := tac ().
Ltac rec x := rec.
Goal True.
Fail foo.
Fail bar.
Fail bar True.
Fail baz.
Fail qux.
Fail mydo ltac:(fun _ _ => idtac).
Fail let tac := (fun _ => idtac) in tac.
Fail (fun _ => idtac).
Fail rec True.
Fail let rec tac x := tac in tac True.
Abort.
|
