blob: ae5d51bae81d136713f29f7a834c8a025a2cf26d (
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
|
(* -*- coq-prog-args: ("-profile-ltac") -*- *)
Require Coq.ZArith.BinInt.
Module WithIdTac.
Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
Ltac foo0 := idtac; sleep.
Ltac foo1 := sleep; foo0.
Ltac foo2 := sleep; foo1.
Goal True.
foo2.
Show Ltac Profile CutOff 47.
constructor.
Qed.
End WithIdTac.
Module TestEval.
Ltac sleep := let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac.
Ltac foo0 := idtac; do 50 (idtac; sleep).
Ltac foo1 := sleep; foo0.
Ltac foo2 := sleep; foo1.
Goal True.
Reset Ltac Profile.
foo2.
Show Ltac Profile CutOff 47.
constructor.
Qed.
End TestEval.
|
