From edb7a97487cb5e38bb284472eacfd1b58fa97f84 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 21 Nov 2016 07:00:31 +0100
Subject: Fixing space in printing "Context".

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

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 75271e21ea..9533833212 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -913,7 +913,7 @@ module Make
       | VernacContext l ->
         return (
           hov 1 (
-            keyword "Context" ++ spc () ++ pr_and_type_binders_arg l)
+            keyword "Context" ++ pr_and_type_binders_arg l)
         )
 
       | VernacDeclareInstances insts ->
-- 
cgit v1.2.3