aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/ltacprof.v
blob: d5552695c48210004642ca08cce62e744fef4286 (plain)
1
2
3
4
5
6
7
8
(** 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.