Xml.token is now namespace-aware. As a consequence, xml2Gdomexmath is

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

diff --git a/helm/ocaml/cic_transformations/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml
index 8cce6e1e39a116e8200bed2a35f2dc339e8841be..bda66841cc2cfd82bbda49aa80a24694dcfd3eb0 100644 (file)
--- a/helm/ocaml/cic_transformations/sequentPp.ml
+++ b/helm/ocaml/cic_transformations/sequentPp.ml
@@ -90,8 +90,8 @@ module XmlPp =
                  [< s ;
                     X.xml_nempty
                      (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
-                     ["name",(match n with Cic.Name n -> n | _ -> assert false);
-                      "id",hid]
+                     [None,"name",(match n with Cic.Name n -> n | _ -> assert false);
+                      None,"id",hid]
                      (Cic2Xml.print_term ~ids_to_inner_sorts acic)
                  >], (entry::context), (hid::idrefs)
              | None ->
@@ -103,7 +103,8 @@ module XmlPp =
        let acic = acic_of_cic_context context final_idrefs goal None in
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
             X.xml_cdata ("<!DOCTYPE Sequent SYSTEM \"" ^ dtdname ^ "\">\n");
-            X.xml_nempty "Sequent" ["no",string_of_int metano;"id",sequent_id]
+            X.xml_nempty "Sequent"
+             [None,"no",string_of_int metano;None,"id",sequent_id]
              [< final_s ;
                 Xml.xml_nempty "Goal" []
                  (Cic2Xml.print_term ~ids_to_inner_sorts acic)