TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
in
CicNotationPres.box_of_mpres
- (CicNotationPres.render ids_to_uris
+ (CicNotationPres.render
+ ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris)
(TermContentPres.pp_ast ast)))
-let nsequent2pres ~subst =
+let nsequent2pres ~ids_to_nrefs ~subst =
+ let lookup_uri id =
+ try
+ let nref = Hashtbl.find ids_to_nrefs id in
+ Some (NReference.string_of_reference nref)
+ with Not_found -> None
+ in
sequent2pres0
- (fun term ->
- let ast = NTermCicContent.nast_of_cic ~subst term in
- CicNotationPres.box_of_mpres
- (CicNotationPres.render (Hashtbl.create 1)
- (TermContentPres.pp_ast ast)))
+ (fun ast ->
+ CicNotationPres.box_of_mpres
+ (CicNotationPres.render ~lookup_uri
+ (TermContentPres.pp_ast ast)))