handled difference associativity for the same level of the extensible grammar

[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 3118753f6088236ec11d182111555a235a96854d..639ae48e0e62e00d4f7be4c7f724fd1e577896e8 100644 (file)
--- 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 ->