[< s ;
X.xml_nempty
(match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
- ["name",(match n with Cic.Name n -> n | _ -> assert false);
- "id",hid]
+ [None,"name",(match n with Cic.Name n -> n | _ -> assert false);
+ None,"id",hid]
(Cic2Xml.print_term ~ids_to_inner_sorts acic)
>], (entry::context), (hid::idrefs)
| None ->
let acic = acic_of_cic_context context final_idrefs goal None in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Sequent SYSTEM \"" ^ dtdname ^ "\">\n");
- X.xml_nempty "Sequent" ["no",string_of_int metano;"id",sequent_id]
+ X.xml_nempty "Sequent"
+ [None,"no",string_of_int metano;None,"id",sequent_id]
[< final_s ;
Xml.xml_nempty "Goal" []
(Cic2Xml.print_term ~ids_to_inner_sorts acic)