diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-25 16:52:00 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-02-01 16:20:16 +0000 |
| commit | 5b8b60508d74bfe5e436ce182889ad8ee6ca3983 (patch) | |
| tree | 3a9bdfb906444e1f041af3e09df0cc49f911839b /printing | |
| parent | e42f575b22ff2d2a69951227e8c2dd67fd0ab3ee (diff) | |
[vernac] Mutual theorems (VernacStartTheoremProof) always have names
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index cea2ec35a..950246c53 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()) ++ |