diff options
Diffstat (limited to 'ltac/profile_ltac.ml')
-rw-r--r-- | ltac/profile_ltac.ml | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index b008d389f..405c494a6 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -150,18 +150,17 @@ let string_of_call ck = let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in CString.strip s -let exit_tactic start_time add_total c = - try - let node :: stack' = !stack in - let parent = List.hd stack' in - stack := stack'; - if add_total then Hashtbl.remove on_stack (string_of_call c); - let diff = time () -. start_time in - parent.entry.local <- parent.entry.local -. diff; - let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in - add_entry node.entry add_total node'; - with Failure ("hd") -> (* oops, our stack is invalid *) - encounter_multi_success_backtracking () +let exit_tactic start_time add_total c = match !stack with +| [] | [_] -> + (* oops, our stack is invalid *) + encounter_multi_success_backtracking () +| node :: (parent :: _ as stack') -> + stack := stack'; + if add_total then Hashtbl.remove on_stack (string_of_call c); + let diff = time () -. start_time in + parent.entry.local <- parent.entry.local -. diff; + let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in + add_entry node.entry add_total node' let tclFINALLY tac (finally : unit Proofview.tactic) = let open Proofview.Notations in |