diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:03 +0200 |
| commit | 1fe4593d355fcf305e36ebf4abf7e290ec37fab1 (patch) | |
| tree | cfa6eed557922f2f2434c4ab1d2e738d2a2da072 | |
| parent | 27a6d4a87058fdbc93c4575ea8c7af68237787a4 (diff) | |
Revert "Fixing printing of keeping hyp on the fly."
This reverts commit d408e09e5366899f4313f433cc9507ea92458c49.
| -rw-r--r-- | printing/pptactic.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 477758551..6f891c5f8 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 |