Content2pres.ncontext2pres
((new NCicPp.status)#ppcontext ~metasenv ~subst)
-let ntxt_of_cic_subst ~map_unicode_to_tex size status ~metasenv ?use_subst subst =
+let ntxt_of_cic_subst ~map_unicode_to_tex:_ _size _status ~metasenv ?use_subst subst =
[],
"<<<high level printer for subst not implemented; low-level printing:>>>\n" ^
(new NCicPp.status)#ppsubst ~metasenv ?use_subst subst
object(self)
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
+ method ppterm ~context ~subst ~metasenv ?margin:(_) ?inside_fix:(_) t =
+ 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
+ method ppcontext ?sep:(_) ~subst ~metasenv context =
+ 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