X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;fp=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=3e48d36792d3a33ce508e07dfa48179ae7f42a6c;hb=f528a32d327fef04d89d80b26e9db2fb17969100;hp=e784a8302173f188ac0d515b5cca26a29e194528;hpb=15fd88968e181fdafa0fecf82c5a32661c0f4e7e;p=helm.git

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 =