From 3893944e46cd06ae9db422c1fa355f7131130d9a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 27 Jul 2005 07:51:57 +0000 Subject: [PATCH] improved debugging pretty printing of xref --- helm/ocaml/cic_notation/cicNotationPp.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 -- 2.39.2