aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.ml')
-rw-r--r--stm/stm.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index b9247fff04..01edc9d2d8 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -476,7 +476,7 @@ end = struct (* {{{ *)
let mk_branch_name { expr = x } = Branch.make
(let rec aux x = match x with
| VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
- | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i
+ | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i
| VernacTime (_, e)
| VernacTimeout (_, e) -> aux e
| _ -> "branch" in aux x)