diff options
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |