From 40aca595dd8e26373bfa4f6b6d4cd7d43a933210 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 11 Dec 2017 02:23:10 -0500
Subject: Add tactics to reset and display the Ltac profile

This is useful for tactics that run a bunch of tests and need to display
the profile for each of them.
---
 test-suite/bugs/closed/6378.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/6378.v b/test-suite/bugs/closed/6378.v
index d0ef090d08..68ae7961dd 100644
--- a/test-suite/bugs/closed/6378.v
+++ b/test-suite/bugs/closed/6378.v
@@ -1,4 +1,18 @@
+Require Import Coq.ZArith.ZArith.
+Ltac profile_constr tac :=
+  let dummy := match goal with _ => reset ltac profile; start ltac profiling end in
+  let ret := match goal with _ => tac () end in
+  let dummy := match goal with _ => stop ltac profiling; show ltac profile end in
+  pose 1.
+
+Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl).
+
 Goal True.
   start ltac profiling.
+  reset ltac profile.
+  reset ltac profile.
   stop ltac profiling.
+  time profile_constr slow.
+  show ltac profile cutoff 0.
+  show ltac profile "slow".
 Abort.
-- 
cgit v1.2.3