X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser2.ml;h=154b294ce7daff797cbd3d27fa1f0e85292332e4;hb=b57c31a1593872c181249135bc05ebd9a72f523b;hp=4865c6e4a584fcb82bf05e2bb300cd549353e9e6;hpb=82466efd82082c6101d1c2c0c217f681b37160e8;p=helm.git

diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml
index 4865c6e4a..154b294ce 100644
--- a/helm/ocaml/cic/cicParser2.ml
+++ b/helm/ocaml/cic/cicParser2.ml
@@ -152,6 +152,7 @@ let get_conjs_value_type l =
       [] -> (c, v, t)
     | conj::tl when conj#node_type = D.T_element "Conjecture" ->
        let no = int_of_attr (conj#attribute "no") in
+       let xid = string_of_attr (conj#attribute "id") in
        let typ,canonical_context =
         match List.rev (conj#sub_nodes) with
            [] -> raise (IllFormedXml 13)
@@ -162,17 +163,21 @@ let get_conjs_value_type l =
                match n#node_type with
                   D.T_element "Decl" ->
                    let name = name_of_attr (n#attribute "name") in
+                   let hid = string_of_attr (n#attribute "id") in
                    let term = (get_content n)#extension#to_cic_term in
-                    Some (name,Cic.ADecl term)
+                    hid,Some (name,Cic.ADecl term)
                 | D.T_element "Def" ->
                    let name = name_of_attr (n#attribute "name") in
+                   let hid = string_of_attr (n#attribute "id") in
                    let term = (get_content n)#extension#to_cic_term in
-                    Some (name,Cic.ADef term)
-                | D.T_element "Hidden" -> None
+                    hid,Some (name,Cic.ADef term)
+                | D.T_element "Hidden" ->
+                   let hid = string_of_attr (n#attribute "id") in
+                    hid,None
                 | _ -> raise (IllFormedXml 14)
              ) canonical_context
        in
-        rget ((no, canonical_context, typ)::c, v, t) tl
+        rget ((xid, no, canonical_context, typ)::c, v, t) tl
     | value::tl when value#node_type = D.T_element "body" ->
        let v' = (get_content value)#extension#to_cic_term in
         (match v with