From d82c87e40a85be184ede1f9a2fde04dd8f48bb74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 16 Apr 2016 20:04:49 +0200
Subject: Simplification in ppvernac.ml.

---
 printing/ppvernac.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index bf7d758515..17926055e8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -86,10 +86,6 @@ 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"
@@ -271,7 +267,7 @@ module Make
       pr_opt (fun sc -> str ": " ++ str sc) scopt
 
   let pr_binders_arg =
-    pr_ne_sep spc pr_binders
+    pr_non_empty_arg pr_binders
 
   let pr_and_type_binders_arg bl =
     pr_binders_arg bl
-- 
cgit v1.2.3