From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 20 Sep 2005 15:29:58 +0000 (+0000)
Subject: pretty printing of literals is now subject to the debug setting
X-Git-Tag: LAST_BEFORE_NEW~79
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f528a32d327fef04d89d80b26e9db2fb17969100;p=helm.git

pretty printing of literals is now subject to the debug setting
---

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 =