X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FapplyTransformation.ml;h=0528a01ce1bcd6b02bcc317fd70d2b54fd383c72;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=a911742b05e980b810aaf8f7b74db4078ea197a3;hpb=b3be8ee41041a90005740cfa106109e0c83db13f;p=helm.git diff --git a/matitaB/matita/applyTransformation.ml b/matitaB/matita/applyTransformation.ml index a911742b0..0528a01ce 100644 --- a/matitaB/matita/applyTransformation.ml +++ b/matitaB/matita/applyTransformation.ml @@ -83,11 +83,11 @@ let ntxt_of_cic_subst ~map_unicode_to_tex size status ~metasenv ?use_subst subst *) -class status = +class status uid = object(self) - inherit Interpretations.status - inherit TermContentPres.status - inherit NCicPp.status + inherit Interpretations.status uid + inherit TermContentPres.status uid + inherit NCicPp.status uid (* method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t = NCicPp.ppterm ~metasenv ~subst ~context t @@ -101,7 +101,7 @@ class status = method ppmetasenv ~subst metasenv = String.concat "\n" (List.map - (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 20 self + (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 50 self ~metasenv ~subst m) metasenv) (* method ppobj obj =