From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 27 Jul 2005 07:51:57 +0000 (+0000)
Subject: improved debugging pretty printing of xref
X-Git-Tag: V_0_7_2~54
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3893944e46cd06ae9db422c1fa355f7131130d9a;p=helm.git

improved debugging pretty printing of xref
---

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