From 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Thu, 25 Jan 2018 16:52:00 +0000
Subject: [vernac] Mutual theorems (VernacStartTheoremProof) always have names

---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm/stm.ml')

diff --git a/stm/stm.ml b/stm/stm.ml
index ba6c90011..ef599fd48 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -548,7 +548,7 @@ end = struct (* {{{ *)
   let mk_branch_name { expr = x } = Branch.make
     (match Vernacprop.under_control x with
     | VernacDefinition (_,((_, Name i),_),_) -> Id.to_string i
-    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i
+    | VernacStartTheoremProof (_,[((_,i),_),_]) -> Id.to_string i
     | _ -> "branch")
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
-- 
cgit v1.2.3