Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/6378.v b/test-suite/bugs/closed/6378.v
new file mode 100644
index 00000000..68ae7961
--- /dev/null
+++ b/test-suite/bugs/closed/6378.v
@@ -0,0 +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.