From 001ae6adf5c3a926058af6a431626f4553c3f4d0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:03 +0200
Subject: Revert "Fixing printing of Polymorphic/Monomorphic."

This reverts commit 094ed756fcef1ac5118dc5134a7369252efec933.
---
 printing/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 6670aa41ab..4056115785 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -518,7 +518,7 @@ module Make
       match v with
         | VernacPolymorphic (poly, v) ->
           let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
-          return (s ++ spc () ++ pr_vernac v)
+          return (s ++ pr_vernac v)
         | VernacProgram v ->
           return (keyword "Program" ++ spc() ++ pr_vernac v)
         | VernacLocal (local, v) ->
-- 
cgit v1.2.3