]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/matita/cicMathView.ml
update in ground_2 static_2 basic_2
[helm.git] / matitaB / matita / cicMathView.ml
index 685324580dca09012135aec314f655889b296457..effa760014fe0bb87ff4734c733f92d3b03022c1 100644 (file)
@@ -637,7 +637,7 @@ object (self)
     let sequent = List.assoc metano metasenv in
     let txt =
      ApplyTransformation.ntxt_of_cic_sequent
-      ~map_unicode_to_tex:false 80 status ~metasenv ~subst (metano,sequent)
+      ~map_unicode_to_tex:false 50 status ~metasenv ~subst (metano,sequent)
     in
     (* MATITA 1.0 if BuildTimeConf.debug then begin
       let name =
@@ -651,7 +651,7 @@ object (self)
    'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit
    = fun status obj ->
     let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false
-    80 status obj in
+    20 status obj in
 (*
     self#set_cic_info
       (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));