diff options
| -rw-r--r-- | ltac/profile_ltac.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index d2b7c7075..fe591c775 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -73,7 +73,7 @@ module Local = Summary.Local let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root] -let reset_profile () = +let reset_profile_tmp () = Local.(stack := [empty_treenode root]); encountered_multi_success_backtracking := false @@ -295,7 +295,7 @@ let exit_tactic start_time c = | [] | [_] -> (* oops, our stack is invalid *) encounter_multi_success_backtracking (); - reset_profile () + reset_profile_tmp () | node :: (parent :: rest as full_stack) -> let name = string_of_call c in if not (String.equal name node.name) then @@ -330,7 +330,7 @@ let exit_tactic start_time c = (* Calls are over, we reset the stack and send back data *) if rest == [] && get_profiling () then begin assert(String.equal root parent.name); - reset_profile (); + reset_profile_tmp (); feedback_results parent end @@ -381,6 +381,10 @@ let _ = data := SM.add s (merge_roots results other_results) !data | _ -> ())) +let reset_profile () = + reset_profile_tmp (); + data := SM.empty + (* ******************** *) let print_results_filter ~filter = |