Many many improvements:

[helm.git] / helm / gTopLevel / cic2Xml.ml

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index a25d7f6709ce20cb0bdd17793b3e1a585c46521f..f04df2f2f6bf4cce1e4b0f376723920dd9f76058 100644 (file)
--- 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,32 @@ 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 (n,canonical_context,t) ->
                [< i ;
                   X.xml_nempty "Conjecture" ["no",(string_of_int n)]
-                   (print_term curi ids_to_inner_sorts t)
+                   [< List.fold_left
+                       (fun i t ->
+                         [< (match t with
+                               Some (n,C.ADecl t) ->
+                                X.xml_nempty "Decl"
+                                 (match n with
+                                     C.Name n' -> ["name",n']
+                                   | C.Anonimous -> [])
+                                 (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 -> [])
+                                 (print_term curi ids_to_inner_sorts t)
+                             | None -> X.xml_empty "Hidden" []
+                            ) ;
+                            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) ;