From 9ff2c9d8d042c9989b6a8138c308398c49ae116f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 23 Jun 2015 10:12:41 +0200
Subject: LtacProf for Coq trunk

This add LtacProfiling.  Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
---
 test-suite/success/ltacprof.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/success/ltacprof.v

(limited to 'test-suite')

diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v
new file mode 100644
index 0000000000..6b73443d6a
--- /dev/null
+++ b/test-suite/success/ltacprof.v
@@ -0,0 +1,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.
-- 
cgit v1.2.3