From 00f1839a2cee1cb1fa4dc207391c4a5bb588f71a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 15:40:40 +0100
Subject: Fixing space in printing several list of implicit arguments.

---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index be15879184..75271e21ea 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1060,7 +1060,7 @@ module Make
               in
               print_arguments nargs args ++
                 if not (List.is_empty more_implicits) then
-                  str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits
+                  prlist (fun l -> str"," ++ print_implicits l) more_implicits
                 else (mt ()) ++
                 (if not (List.is_empty mods) then str" : " else str"") ++
                   prlist_with_sep (fun () -> str", " ++ spc()) (function
-- 
cgit v1.2.3