X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=cb67202a5a6e73554303e44ace1bec4645cbe68a;hb=08791e80816548121e81e04d3ead8c9a5171d033;hp=a3e4f46211a97a2b5fef1399fd6c50a063e3f9ed;hpb=3d63cb9ed38f05c679fc3284a5b3bb4d92e52296;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index a3e4f4621..cb67202a5 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -44,6 +44,8 @@ let pp_literal l =
     | `Number s -> s)
 
 let rec pp_term = function
+  | AttributedTerm (`Href _, term) when print_attributes ->
+      sprintf "#[%s]" (pp_term term)
   | AttributedTerm (_, term) when print_attributes ->
       sprintf "@[%s]" (pp_term term)
   | AttributedTerm (_, term) -> pp_term term