X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=639ae48e0e62e00d4f7be4c7f724fd1e577896e8;hb=0c04e1f673d69ac652c15705863931c45e107515;hp=3118753f6088236ec11d182111555a235a96854d;hpb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 3118753f6..639ae48e0 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -53,9 +53,7 @@ let rec pp_term ?(pp_parens = true) t =
         sprintf "#[%s]" (pp_term term)
     | AttributedTerm (_, term) when print_attributes ->
         sprintf "@[%s]" (pp_term term) *)
-    | AttributedTerm (`Raw (text, None), _) -> text
-    | AttributedTerm (`Raw (text, Some `Ast), _) -> sprintf "@{%s}" text
-    | AttributedTerm (`Raw (text, Some `Meta), _) -> sprintf "${%s}" text
+    | AttributedTerm (`Raw text, _) -> text
     | AttributedTerm (_, term) -> pp_term ~pp_parens:false term
 
     | Appl terms ->