X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2Xml.ml;h=ad1d1f8818fb244190075feb9b0223e5db4c77ad;hb=b57c31a1593872c181249135bc05ebd9a72f523b;hp=f04df2f2f6bf4cce1e4b0f376723920dd9f76058;hpb=82466efd82082c6101d1c2c0c217f681b37160e8;p=helm.git

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index f04df2f2f..ad1d1f881 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -185,25 +185,26 @@ let print_object curi ids_to_inner_sorts =
        C.ACurrentProof (id,n,conjectures,bo,ty) ->
         X.xml_nempty "CurrentProof" ["name",n ; "id", id]
          [< List.fold_left
-             (fun i (n,canonical_context,t) ->
+             (fun i (cid,n,canonical_context,t) ->
                [< i ;
-                  X.xml_nempty "Conjecture" ["no",(string_of_int n)]
+                  X.xml_nempty "Conjecture"
+                   ["id", cid ; "no",(string_of_int n)]
                    [< List.fold_left
-                       (fun i t ->
+                       (fun i (hid,t) ->
                          [< (match t with
                                Some (n,C.ADecl t) ->
                                 X.xml_nempty "Decl"
                                  (match n with
-                                     C.Name n' -> ["name",n']
-                                   | C.Anonimous -> [])
+                                     C.Name n' -> ["id",hid;"name",n']
+                                   | C.Anonimous -> ["id",hid])
                                  (print_term curi ids_to_inner_sorts t)
                              | Some (n,C.ADef t) ->
                                 X.xml_nempty "Def"
                                  (match n with
-                                     C.Name n' -> ["name",n']
-                                   | C.Anonimous -> [])
+                                     C.Name n' -> ["id",hid;"name",n']
+                                   | C.Anonimous -> ["id",hid])
                                  (print_term curi ids_to_inner_sorts t)
-                             | None -> X.xml_empty "Hidden" []
+                             | None -> X.xml_empty "Hidden" ["id",hid]
                             ) ;
                             i
                          >]