in
context2pres
(match skip_initial_lambdas_internal with
- Some (`Now n) -> snd (HExtlib.split_nth "CP 1" n p.Con.proof_context)
+ Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context)
| _ -> p.Con.proof_context)
presacontext
in
TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
in
CicNotationPres.box_of_mpres
- (CicNotationPres.render ids_to_uris ~prec
+ (CicNotationPres.render
+ ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec
(TermContentPres.pp_ast ast)))