]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/matita/applyTransformation.ml
update in ground_2 and basic_2
[helm.git] / matitaB / matita / applyTransformation.ml
index f99c67f8b1ab6161d2b48c4c949d7779eab9ac29..0528a01ce1bcd6b02bcc317fd70d2b54fd383c72 100644 (file)
@@ -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 80 self
+      (fun m -> ntxt_of_cic_sequent ~map_unicode_to_tex:true 50 self
         ~metasenv ~subst m) metasenv)
 (*
   method ppobj obj =