diff options
Diffstat (limited to 'ltac/profile_ltac.ml')
| -rw-r--r-- | ltac/profile_ltac.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 9081fd3e9..f332e1a0d 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -32,10 +32,14 @@ let is_new_call () = let b = !new_call in new_call := false; b profiling results will be off. *) let encountered_multi_success_backtracking = ref false +let warn_profile_backtracking = + CWarnings.create ~name:"profile-backtracking" ~category:"ltac" + (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \ + into multi-success tactics; profiling results may be wildly inaccurate.") + let warn_encountered_multi_success_backtracking () = if !encountered_multi_success_backtracking then - Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking \ - into multi-success tactics; profiling results may be wildly inaccurate.") + warn_profile_backtracking () let encounter_multi_success_backtracking () = if not !encountered_multi_success_backtracking |