test-suite/success/ltacprof.v


1
2
3
4
5
6
7
8

(** Some LtacProf tests *)

Start Profiling.
Ltac multi := (idtac + idtac).
Goal True.
  try (multi; fail). (* Anomaly: Uncaught exception Failure("hd"). Please report. *)
Admitted.
Show Profile.