blob: 91331a1de5da7355f7fd7963c0b07ba177c0760a (
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.
|
