X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FsequentPp.ml;h=bda66841cc2cfd82bbda49aa80a24694dcfd3eb0;hb=6f65a2e518d723ea722b23bfd9fa0162ff8be457;hp=8cce6e1e39a116e8200bed2a35f2dc339e8841be;hpb=b266dce15b2f669a70daaee3bd0887f8d9c345b2;p=helm.git

diff --git a/helm/ocaml/cic_transformations/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml
index 8cce6e1e3..bda66841c 100644
--- 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)