X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fmpresentation.ml;h=1303d1eb7a4dc19d4effa0122074b13c54d002d1;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=db05f31bea0dfc9cd121bda41c3814bbe8befb6e;hpb=5994e8316c4ab219a06b735afdc94ecf5dd73f8e;p=helm.git

diff --git a/helm/ocaml/cic_notation/mpresentation.ml b/helm/ocaml/cic_notation/mpresentation.ml
index db05f31be..1303d1eb7 100644
--- a/helm/ocaml/cic_notation/mpresentation.ml
+++ b/helm/ocaml/cic_notation/mpresentation.ml
@@ -108,7 +108,14 @@ let print_mpres obj_printer mpres =
     function
       Mi (attr,s) -> X.xml_nempty ~prefix "mi" attr (X.xml_cdata s)
     | Mn (attr,s) -> X.xml_nempty ~prefix "mn" attr (X.xml_cdata s)
-    | Mo (attr,s) -> X.xml_nempty ~prefix "mo" attr (X.xml_cdata s)
+    | Mo (attr,s) ->
+        let s =
+          let len = String.length s in
+          if len > 1 && s.[0] = '\\'
+          then String.sub s 1 (len - 1)
+          else s
+        in
+        X.xml_nempty ~prefix "mo" attr (X.xml_cdata s)
     | Mtext (attr,s) -> X.xml_nempty ~prefix "mtext" attr (X.xml_cdata s)
     | Mspace attr -> X.xml_empty ~prefix "mspace" attr
     | Ms (attr,s) -> X.xml_nempty ~prefix "ms" attr (X.xml_cdata s)