X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2Fcic2Xml.ml;h=ad1d1f8818fb244190075feb9b0223e5db4c77ad;hb=c929e791b0eca1e75694a663a2f6ada9f0ff9534;hp=a25d7f6709ce20cb0bdd17793b3e1a585c46521f;hpb=3e0de84a7ef35919fc3c4722c525fcc6cbf68bb5;p=helm.git

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index a25d7f670..ad1d1f881 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -49,9 +49,17 @@ let print_term curi ids_to_inner_sorts =
           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
             (U.name_of_uri uri) ;
            "id",id ; "sort",sort]
-     | C.AMeta (id,n) ->
+     | C.AMeta (id,n,l) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_empty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
+         X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
+          (List.fold_left
+            (fun i t ->
+              match t with
+                 Some t' ->
+                  [< i ; X.xml_nempty "substitution" [] (aux t') >]
+               | None ->
+                  [< i ; X.xml_empty "substitution" [] >]
+            ) [< >] l)
      | C.ASort (id,s) ->
         let string_of_sort =
          function
@@ -177,10 +185,33 @@ 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,t) ->
+             (fun i (cid,n,canonical_context,t) ->
                [< i ;
-                  X.xml_nempty "Conjecture" ["no",(string_of_int n)]
-                   (print_term curi ids_to_inner_sorts t)
+                  X.xml_nempty "Conjecture"
+                   ["id", cid ; "no",(string_of_int n)]
+                   [< List.fold_left
+                       (fun i (hid,t) ->
+                         [< (match t with
+                               Some (n,C.ADecl t) ->
+                                X.xml_nempty "Decl"
+                                 (match n with
+                                     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' -> ["id",hid;"name",n']
+                                   | C.Anonimous -> ["id",hid])
+                                 (print_term curi ids_to_inner_sorts t)
+                             | None -> X.xml_empty "Hidden" ["id",hid]
+                            ) ;
+                            i
+                         >]
+                       ) [< >] canonical_context ;
+                      X.xml_nempty "Goal" []
+                       (print_term curi ids_to_inner_sorts t)
+                   >]
                >])
              [<>] conjectures ;
             X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;