From b5cc4ac65764b0866bf57caa6f9aa7fa631eabf1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 9 Apr 2016 16:14:29 +0200
Subject: Fixing extra space in printing inductive types with no explicit type
 given.

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

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 55f8f909f0..0b761881dc 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -778,8 +778,8 @@ module Make
             hov 0 (
               str key ++ spc() ++
                 (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++
-                pr_and_type_binders_arg indpar ++ spc() ++
-                Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
+                pr_and_type_binders_arg indpar ++
+                pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) s ++
                 str" :=") ++ pr_constructor_list k lc ++
               prlist (pr_decl_notation pr_constr) ntn
           in
-- 
cgit v1.2.3