blob: cc7ccc694cd91ca6233ad85330b7b7311f8512f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
Ltac bar k := k tt.
(* The next tactic definition seems to get stuck when processing in PG.
It works fine typed into coqtop and also works if a couple of the
match lines are removed.
It does seem to be something to do with the line length, as if
the lines are commented out the same problem happens.
See http://proofgeneral.inf.ed.ac.uk/trac/ticket/447
*)
Ltac foo x :=
bar ltac:(fun a =>
bar ltac:(fun b =>
bar ltac:(fun c =>
bar ltac:(fun d =>
bar ltac:(fun e =>
bar ltac:(fun f =>
bar ltac:(fun g =>
bar ltac:(fun h =>
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
let x := match tt with | tt => constr:(1) end in
idtac)))))))).
Ltac wim x := foo x.
|
