From 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Apr 2016 11:50:33 +0200
Subject: Protect printing of ltac's "context [...]" from possible collision
 with user-level notations by inserting spaces.

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

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 4777585516..a31b8b4dae 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