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

---
 printing/ppvernac.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index cea2ec35a0..950246c531 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -391,8 +391,6 @@ open Decl_kinds
     ++ prlist (pr_decl_notation pr_constr) ntn
 
   let pr_statement head (idpl,(bl,c)) =
-    assert (not (Option.is_empty idpl));
-    let idpl = Option.get idpl in
     hov 2
       (head ++ spc() ++ pr_ident_decl idpl ++ spc() ++
          (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
-- 
cgit v1.2.3