aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--printing/pptactic.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 4777585516..6f891c5f80 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -250,10 +250,8 @@ module Make
| NoBindings -> mt ()
let pr_clear_flag clear_flag pp x =
- match clear_flag with
- | Some false -> surround (pp x)
- | Some true -> str ">" ++ pp x
- | None -> pp x
+ (match clear_flag with Some false -> str "!" | Some true -> str ">" | None -> mt())
+ ++ pp x
let pr_with_bindings prc prlc (c,bl) =
prc c ++ pr_bindings prc prlc bl