let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
mml_of_cic_sequent metasenv sequent
in
let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
mml_of_cic_sequent metasenv sequent
in
ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml ());
current_infos <-
Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml ());
current_infos <-
Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)