(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 = NTermCicContent.map_sequent sequent in
+ let content_sequent = NTermCicContent.nmap_sequent ~subst sequent in
let pres_sequent =
- Sequent2pres.nsequent2pres content_sequent in
+ Sequent2pres.nsequent2pres subst content_sequent in
let xmlpres = mpres_document pres_sequent in
Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres