LtacProf now handles multi-success backtracking

Fixes #12196

1 files changed, 17 insertions, 0 deletions

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.