strip heading '\' on Mo s

diff --git a/helm/ocaml/cic_notation/mpresentation.ml b/helm/ocaml/cic_notation/mpresentation.ml
index db05f31bea0dfc9cd121bda41c3814bbe8befb6e..1303d1eb7a4dc19d4effa0122074b13c54d002d1 100644 (file)
--- 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)