From c86d8e5314d1a1a8ef3776ef0ba25b3f592f48da Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 3 Jun 2017 06:55:05 +0200
Subject: [stm] Solve bug 5577 "STM branch name is incorrect with Time"

---
 stm/stm.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 2057496f4b..07219f2547 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -474,10 +474,12 @@ end = struct (* {{{ *)
     vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
   let reachable id = reachable !vcs id
   let mk_branch_name { expr = x } = Branch.make
-    (match x with
+    (let rec aux x = match x with
     | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
     | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i
-    | _ -> "branch")
+    | VernacTime (_, e)
+    | VernacTimeout (_, e) -> aux e
+    | _ -> "branch" in aux x)
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
   let get_info id =
-- 
cgit v1.2.3