From 1093c5e758f796b9dce3d870cb05f2c8a89bef43 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:02 +0200
Subject: Revert "Fixing extra space in front of terminal in printing vernac."

This reverts commit 834885cb8cbc4d6924a63b898c7a5a32cfd0211c.
---
 printing/miscprint.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/miscprint.ml')

diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 7b2c5695fd..1ab6cc8b90 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -36,9 +36,9 @@ and pr_or_and_intro_pattern prc = function
   | IntroAndPattern pl ->
       str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")"
   | IntroOrPattern pll ->
-      str "[" ++
+      str "[ " ++
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
-      ++ str "]"
+      ++ str " ]"
 
 (** Printing of [move_location] *)
 
-- 
cgit v1.2.3