blob: f40f40c2bb6b36e85a58e35344c96e19cb1ec75b (
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
|
(** Some LtacProf tests *)
Set Ltac Profiling.
Ltac multi := (idtac + idtac).
Goal True.
try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *)
Admitted.
Show Ltac Profile.
(* backtracking across profiler manipulation *)
Unset Ltac Profiling.
Reset Ltac Profile.
Fixpoint slow (n : nat) : unit
:= match n with
| 0 => tt
| S n => fst (slow n, slow n)
end.
Ltac slow := idtac; let v := eval cbv in (slow 16) in idtac.
Ltac multi2 :=
try (((idtac; slow) + (start ltac profiling; slow) + (idtac; slow) + (slow; stop ltac profiling; slow) + slow + (start ltac profiling; (idtac + slow); ((stop ltac profiling + idtac); fail))); slow; fail); slow; show ltac profile.
Goal True.
multi2.
Admitted.
|
