From f528a32d327fef04d89d80b26e9db2fb17969100 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 20 Sep 2005 15:29:58 +0000
Subject: [PATCH] pretty printing of literals is now subject to the debug
 setting

---
 helm/ocaml/cic_notation/cicNotationPp.ml | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index e784a8302..3e48d3679 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -40,15 +40,17 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-let pp_literal = function  (* debugging version *)
-  | `Symbol s -> sprintf "symbol(%s)" s
-  | `Keyword s -> sprintf "keyword(%s)" s
-  | `Number s -> sprintf "number(%s)" s
-
-(* let pp_literal = function
-  | `Symbol s
-  | `Keyword s
-  | `Number s -> s *)
+let pp_literal =
+  if debug_printing then
+    (function (* debugging version *)
+      | `Symbol s -> sprintf "symbol(%s)" s
+      | `Keyword s -> sprintf "keyword(%s)" s
+      | `Number s -> sprintf "number(%s)" s)
+  else
+    (function
+      | `Symbol s
+      | `Keyword s
+      | `Number s -> s)
 
 let rec pp_term ?(pp_parens = true) t =
   let t_pp =
-- 
2.39.2