(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
let nmml_of_cic_sequent metasenv subst sequent =
(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
let nmml_of_cic_sequent metasenv subst sequent =
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
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
let mml_of_cic_object obj =
let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
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 =
ids_to_inner_sorts,ids_to_inner_types)))
let nmml_of_cic_object obj =
let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
let xmlpres = mpres_document pres_sequent in
let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
let xmlpres = mpres_document pres_sequent in