LtacProf should correctly handle multi-success tactics

[JasonGross]

Description of the problem

LtacProf currently admits that it cannot handle multi-success tactics:

Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end.
Fixpoint walk (n : nat) := match n with 0 => tt | S n => walk n end.
Ltac slow := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
Ltac slow2 := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)).
Ltac multi := idtac + slow + slow2.
Set Ltac Profiling.
Goal True.
  Time try (multi; fail).
  (* Warning: Ltac Profiler cannot yet handle backtracking into multi-success
 tactics; profiling results may be wildly inaccurate.
 [profile-backtracking,ltac] *)
  Show Ltac Profile.
  (* total time:      0.000s

 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─multi ---------------------------------  47.1%  47.1%       1    0.000s
─slow ----------------------------------  35.3%  35.3%       1    0.000s
─slow2 ---------------------------------  17.6%  17.6%       1    0.000s

 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─multi ---------------------------------  47.1%  47.1%       1    0.000s
─slow ----------------------------------  35.3%  35.3%       1    0.000s
─slow2 ---------------------------------  17.6%  17.6%       1    0.000s

*)

It does something, but the results are quite strange.

Coq Version

8.11.1