let mml_of_cic_sequent metasenv sequent =
let asequent,ids_to_terms,
ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses =
let mml_of_cic_sequent metasenv sequent =
let asequent,ids_to_terms,
ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses =
let content_sequent = Cic2content.map_sequent asequent in
let pres_sequent =
(Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in
let content_sequent = Cic2content.map_sequent asequent in
let pres_sequent =
(Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in
(* Xml.pp_to_outchan xmlpres stdout ; *)
try
Xml2Gdome.document_of_xml Misc.domImpl xmlpres, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
(* Xml.pp_to_outchan xmlpres stdout ; *)
try
Xml2Gdome.document_of_xml Misc.domImpl xmlpres, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
let time2 = Sys.time () in
(* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
let time2 = Sys.time () in
(* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
let time25 = Sys.time () in
(* alternative: printing to file
prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2)));
let time25 = Sys.time () in
(* alternative: printing to file
prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2)));