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

---
 parsing/g_vernac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 316b26f209..3244b0ff2b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -149,8 +149,8 @@ GEXTEND Gram
     [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr;
         l = LIST0
           [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr ->
-          (Some id,(bl,c)) ] ->
-          VernacStartTheoremProof (thm, (Some id,(bl,c))::l)
+          (id,(bl,c)) ] ->
+          VernacStartTheoremProof (thm, (id,(bl,c))::l)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
       | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
-- 
cgit v1.2.3