improved debugging pretty printing of xref

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index b126a3def6c38166107d2f1695a9afccb2262253..9118d1c11d359c4c9767252ee0cb7e290cd6ab9e 100644 (file)
--- 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