From 570dd44feec40ca2be2dd6a4d46ca5378acdce09 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 28 Apr 2020 15:43:13 -0400
Subject: LtacProf now handles multi-success backtracking

Fixes #12196
---
 test-suite/success/ltacprof.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v
index d5552695c4..f40f40c2bb 100644
--- a/test-suite/success/ltacprof.v
+++ b/test-suite/success/ltacprof.v
@@ -6,3 +6,20 @@ Goal True.
   try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *)
 Admitted.
 Show Ltac Profile.
+
+(* backtracking across profiler manipulation *)
+Unset Ltac Profiling.
+Reset Ltac Profile.
+
+Fixpoint slow (n : nat) : unit
+  := match n with
+     | 0 => tt
+     | S n => fst (slow n, slow n)
+     end.
+
+Ltac slow := idtac; let v := eval cbv in (slow 16) in idtac.
+Ltac multi2 :=
+  try (((idtac; slow) + (start ltac profiling; slow) + (idtac; slow) + (slow; stop ltac profiling; slow) + slow + (start ltac profiling; (idtac + slow); ((stop ltac profiling + idtac); fail))); slow; fail); slow; show ltac profile.
+Goal True.
+  multi2.
+Admitted.
-- 
cgit v1.2.3