- let no = int_of_attr (conj#attribute "no")
- and typ = (get_content conj)#extension#to_cic_term in
- rget ((no, typ)::c, v, t) tl
+ 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)
+ | typ::canonical_context ->
+ (get_content typ)#extension#to_cic_term,
+ List.map
+ (function n ->
+ 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
+ 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
+ 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 ((xid, no, canonical_context, typ)::c, v, t) tl