From 142978009a2585a1af82b3081720d680028c2108 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 27 Apr 2016 22:13:03 +0200
Subject: Revert "Simplification in ppvernac.ml."

This reverts commit d82c87e40a85be184ede1f9a2fde04dd8f48bb74.
---
 printing/ppvernac.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 17926055e..bf7d75851 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -86,6 +86,10 @@ module Make
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
 
+  let pr_ne_sep sep pr = function
+  [] -> mt()
+    | l -> sep() ++ pr l
+
   let pr_set_entry_type = function
     | ETName -> str"ident"
     | ETReference -> str"global"
@@ -267,7 +271,7 @@ module Make
       pr_opt (fun sc -> str ": " ++ str sc) scopt
 
   let pr_binders_arg =
-    pr_non_empty_arg pr_binders
+    pr_ne_sep spc pr_binders
 
   let pr_and_type_binders_arg bl =
     pr_binders_arg bl
-- 
cgit v1.2.3