From 1fe4593d355fcf305e36ebf4abf7e290ec37fab1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 27 Apr 2016 22:13:03 +0200
Subject: Revert "Fixing printing of keeping hyp on the fly."

This reverts commit d408e09e5366899f4313f433cc9507ea92458c49.
---
 printing/pptactic.ml | 6 ++----
 1 file 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
-- 
cgit v1.2.3