X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FapplyTransformation.ml;h=df366a9ae633bd032ed2363ea25679c85c8a953c;hb=3c8da07d7a5d7cf0432a83732a6d103f527afaef;hp=705ef7936df0b993176d11093c6f03b7104004c7;hpb=ff3a27b1cbb969303ece080ef78cf53354545e5e;p=helm.git diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index 705ef7936..df366a9ae 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -76,23 +76,23 @@ class status = 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