From 74223731f771f01f71aad219056abc7dd9133631 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:03 +0200
Subject: Revert "Protect printing of ltac's "context [...]" from possible
 collision"

This reverts commit 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd.
---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a31b8b4dae..4777585516 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -194,7 +194,7 @@ module Make
     | ConstrContext ((_,id),c) ->
       hov 0
         (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
-           str "[ " ++ prlc c ++ str " ]")
+           str "[" ++ prlc c ++ str "]")
     | ConstrTypeOf c ->
       hov 1 (keyword "type of" ++ spc() ++ prc c)
     | ConstrTerm c when test c ->
-- 
cgit v1.2.3