Conjectures and Hypotheses inside every conjecture and in the sequents now

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

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index f04df2f2f6bf4cce1e4b0f376723920dd9f76058..ad1d1f8818fb244190075feb9b0223e5db4c77ad 100644 (file)
--- 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
                          >]