version 0.7.1

[helm.git] / helm / ocaml / cic_transformations / ast2pres.ml

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index c82f0fb8add1cfa8366d68a4b2740b89f8e25171..5c1ea95d766be9e53e2afea1fb3856110404b7aa 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -230,7 +230,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
                       append_tail ~tail (Box.Object([],rhs))]) in
         let plbox =
           match pl with
-            [] -> append_tail ~tail (Box.Text([],"[]"))
+          | [] -> append_tail ~tail (Box.Text([],"[]"))
+          | [r] -> (make_rule ~tail:("]" :: tail) "[" r)
           | r::tl -> 
               Box.V([],
                 (make_rule ~tail:[] "[" r) ::
@@ -578,7 +579,7 @@ let box_prefix = "b";;
 
 let add_xml_declaration stream =
   [<
-    Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+    Xml.xml_cdata "<?xml version=\"1.0\" ?>\n" ;
     Xml.xml_cdata "\n";
     Xml.xml_nempty ~prefix:box_prefix "box"
       [ Some "xmlns","m","http://www.w3.org/1998/Math/MathML" ;
@@ -591,7 +592,7 @@ let add_xml_declaration stream =
 let ast2mpresXml ((ast, ids_to_uris) as arg) =
   let astBox = ast2astBox arg in
   let smallAst2mpresXml ast =
-    P.print_mpres (ast2mpres (ast, ids_to_uris))
+    P.print_mpres (fun _ -> assert false) (ast2mpres (ast, ids_to_uris))
   in
   (Box.box2xml ~obj2xml:smallAst2mpresXml astBox)