- synced notation pretty printing with parsing syntax

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

diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml
index 4b47b9014807f37596ff164727f193983e35f2d1..395cab6c29927e01cc1760ec1ac6ccc28e6fd87f 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPres.ml
+++ b/helm/ocaml/cic_notation/cicNotationPres.ml
@@ -33,10 +33,6 @@ let binder_attributes = [None, "mathcolor", "blue"]
 let indent_attributes = [None, "indent", "1em"]
 let keyword_attributes = [None, "mathcolor", "blue"]
 
-let mpres_arrow = Mpresentation.Mo (binder_attributes, "->")
-  (* TODO unicode symbol "to" *)
-let mpres_implicit = Mpresentation.Mtext ([], "?")
-
 let to_unicode s =
   try
     if s.[0] = '\\' then
@@ -212,7 +208,8 @@ let render ids_to_uris =
         assert false
   and aux_attribute xmlattrs mathonly xref pos prec uris t =
     function
-    | `Loc _ -> aux xmlattrs mathonly xref pos prec uris t
+    | `Loc _
+    | `Raw _ -> aux xmlattrs mathonly xref pos prec uris t
     | `Level (child_prec, child_assoc) ->
         let t' = aux xmlattrs mathonly xref pos child_prec uris t in
         add_parens child_prec child_assoc pos prec t'