blob: 8ecd97aa56c43cd95f9e3fd5e4a38ecdcc11dc26 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
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.
|