From 89b3335755910b659d6449d343bed69fae1d609e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 14 Jun 2016 01:17:04 +0200
Subject: Better coding style (semantics).

---
 ltac/profile_ltac.ml | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index b008d389f5..405c494a66 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
-- 
cgit v1.2.3