diff options
| author | Hugo Herbelin | 2016-04-16 22:05:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:30:18 +0200 |
| commit | 4bff0cbf3eaac6ed4cb8670c6096b24ad67a58c0 (patch) | |
| tree | 12a5c2a06d9ae531fb266951da5d18618ecfed2a /printing/pptactic.ml | |
| parent | 364290af0983534c447fec9c5819bccf83a06453 (diff) | |
Fixing printing of keeping hyp on the fly.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 370e1ac317..cfab1408bb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -270,8 +270,10 @@ module Make | NoBindings -> mt () let pr_clear_flag clear_flag pp x = - (match clear_flag with Some false -> str "!" | Some true -> str ">" | None -> mt()) - ++ pp x + match clear_flag with + | Some false -> surround (pp x) + | Some true -> str ">" ++ pp x + | None -> pp x let pr_with_bindings prc prlc (c,bl) = prc c ++ pr_bindings prc prlc bl |