(fun seq -> (new NCicPp.status)#ppmetasenv ~subst [seq])
let ntxt_of_cic_object ~map_unicode_to_tex =
- to_text Interpretations.nmap_obj Content2pres.nobj2pres ~map_unicode_to_tex
+ to_text Interpretations.nmap_cobj Content2pres.nobj2pres ~map_unicode_to_tex
(new NCicPp.status)#ppobj
let ntxt_of_cic_term ~metasenv ~subst ~context =
inherit Interpretations.status
inherit TermContentPres.status
method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
- snd (ntxt_of_cic_term ~map_unicode_to_tex:true 80 self ~metasenv ~subst
+ snd (ntxt_of_cic_term ~map_unicode_to_tex:false 80 self ~metasenv ~subst
~context t)
method ppcontext ?sep ~subst ~metasenv context =
- snd (ntxt_of_cic_context ~map_unicode_to_tex:true 80 self ~metasenv ~subst
+ snd (ntxt_of_cic_context ~map_unicode_to_tex:false 80 self ~metasenv ~subst
context)
method ppsubst ~metasenv ?use_subst subst =
- snd (ntxt_of_cic_subst ~map_unicode_to_tex:true 80 self ~metasenv ?use_subst
+ snd (ntxt_of_cic_subst ~map_unicode_to_tex:false 80 self ~metasenv ?use_subst
subst)
method ppmetasenv ~subst metasenv =
String.concat "\n"
(List.map
- (fun m -> snd (ntxt_of_cic_sequent ~map_unicode_to_tex:true 80 self
+ (fun m -> snd (ntxt_of_cic_sequent ~map_unicode_to_tex:false 80 self
~metasenv ~subst m)) metasenv)
method ppobj obj =
- snd (ntxt_of_cic_object ~map_unicode_to_tex:true 80 self obj)
+ snd (ntxt_of_cic_object ~map_unicode_to_tex:false 80 self obj)
end