X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=9118d1c11d359c4c9767252ee0cb7e290cd6ab9e;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=b126a3def6c38166107d2f1695a9afccb2262253;hpb=08ecc780b3b0a4cac7ed72cf68c310e4eeffa2c1;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index b126a3def..9118d1c11 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -32,7 +32,7 @@ open CicNotationPt
    * be added to the output of pp_term.
    * set to false if you need, for example, cut and paste from matitac output to
    * matitatop *)
-let debug_printing = true
+let debug_printing = false
 
 let pp_binder = function
   | `Lambda -> "lambda"
@@ -55,6 +55,8 @@ let rec pp_term ?(pp_parens = true) t =
     match t with
     | AttributedTerm (`Href _, term) when debug_printing ->
         sprintf "#[%s]" (pp_term ~pp_parens:false term)
+    | AttributedTerm (`IdRef id, term) when debug_printing ->
+        sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term)
     | AttributedTerm (_, term) when debug_printing ->
         sprintf "@[%s]" (pp_term ~pp_parens:false term)
     | AttributedTerm (`Raw text, _) -> text