blob: 3dad6271af8c0836b13681bc622ed1102449a3f7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* -*- coq-prog-args: ("-profile-ltac") -*- *)
Require Coq.ZArith.BinInt.
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.
|
