diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-03 06:55:05 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-03 06:58:13 +0200 |
| commit | c86d8e5314d1a1a8ef3776ef0ba25b3f592f48da (patch) | |
| tree | f9b30d5f55a83299c454310cb02851ecb521c5a9 /stm/stm.ml | |
| parent | a2a98a4015311af83edcf8fc87aa30a5318bead8 (diff) | |
[stm] Solve bug 5577 "STM branch name is incorrect with Time"
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 2057496f4..07219f254 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 = |