From 4e551415f20ad696c319b32b349e4499c2505388 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 17:58:07 +0100
Subject: Protect printing of ltac's "context [...]" from possible collision
 with user-level notations by inserting spaces.

---
 printing/pptactic.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 4b86381b49..fedc62f44f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -219,7 +219,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 ->
@@ -676,9 +676,9 @@ module Make
     | Subterm (b,None,a) ->
     (** ppedrot: we don't make difference between [appcontext] and [context]
         anymore, and the interpretation is governed by a flag instead. *)
-      keyword "context" ++ str" [" ++ pr_pat a ++ str "]"
+      keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]"
     | Subterm (b,Some id,a) ->
-      keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+      keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]"
 
   let pr_match_hyps pr_pat = function
     | Hyp (nal,mp) ->
-- 
cgit v1.2.3