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 =
'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));