blob: 50131470eb2a8e342b0f95b36fa5f9e970043f12 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* -*- coq-prog-args: ("-emacs" "-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.
|
