[] -> (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)
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