diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 74223731f771f01f71aad219056abc7dd9133631 (patch) | |
| tree | 98b8a9a6b131d3727f763b1441d73b2f98be4d3e | |
| parent | 1965c3e4a1f3ab4ab8a777fe3707e71891bac162 (diff) | |
Revert "Protect printing of ltac's "context [...]" from possible collision"
This reverts commit 0d56fda01ecf8b38ef5f9a1fd3552f025972fbcd.
| -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 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 -> |