- let sons = n#sub_nodes
- and id = string_of_xml_attr (n#attribute "id") in
- match sons with
- [s ; t] when
- s#node_type = Pxp_document.T_element "source" &&
- t#node_type = Pxp_document.T_element "target" ->
- let name = cic_attr_of_xml_attr (t#attribute "binder")
- and source = s#extension#to_cic_term
- and target = t#extension#to_cic_term in
- let res = Cic.ALambda (id,ref None,name,source,target) in
- register_id id res ;
- res
- | _ -> raise (IllFormedXml 12)
+ let sons = n#sub_nodes in
+ let rec get_decls_and_target =
+ function
+ [t] when t#node_type = Pxp_document.T_element "target" ->
+ [],t#extension#to_cic_term []
+ | s::tl when s#node_type = Pxp_document.T_element "decl" ->
+ let decls,target = get_decls_and_target tl in
+ let id = string_of_xml_attr (s#attribute "id") in
+ let binder = cic_attr_of_xml_attr (s#attribute "binder") in
+ (id,binder,s#extension#to_cic_term [])::decls, target
+ | _ -> raise (IllFormedXml 12)
+ in
+ let decls,target = get_decls_and_target sons in
+ List.fold_right
+ (fun (id,b,s) t -> Cic.ALambda (id,b,s,t))
+ decls target