(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
let nmml_of_cic_sequent metasenv subst sequent =
- let content_sequent,ids_to_refs =
+ let content_sequent,ids_to_refs,ids_to_father_ids =
NTermCicContent.nmap_sequent ~subst sequent in
let pres_sequent =
Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
let xmlpres = mpres_document pres_sequent in
- Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
+ Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,ids_to_father_ids
let mml_of_cic_object obj =
let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_inner_sorts,ids_to_inner_types)))
let nmml_of_cic_object obj =
- let cobj,ids_to_nrefs = NTermCicContent.nmap_obj obj in
+ let cobj,ids_to_nrefs,ids_to_father_ids = NTermCicContent.nmap_obj obj in
let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
let xmlpres = mpres_document pres_sequent in
- Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
+ Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,ids_to_father_ids
;;
let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =