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

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

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index d954ae9031..8e0fe54c55 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -210,7 +210,7 @@ type typeclass_constraint = name_decl * binding_kind * constr_expr
 and typeclass_context = typeclass_constraint list
 
 type proof_expr =
-  ident_decl option * (local_binder_expr list * constr_expr)
+  ident_decl * (local_binder_expr list * constr_expr)
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
-- 
cgit v1.2.3