X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=6e92cfa95a43fbfc35acf6f01eb622d560286fee;hb=2bd3b029f7f67d9c616b7756278573cc9e96510c;hp=fe8d9e569d24a38a62c77b1d2bc1c1b310e62288;hpb=863eeec8251791046ea6ea487286eb1434520725;p=helm.git diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index fe8d9e569..6e92cfa95 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -78,7 +78,7 @@ let txt_of_cic_sequent_conclusion size metasenv sequent = let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in let t = TermContentPres.pp_ast t in let t = CicNotationPres.render ids_to_uris t in - BoxPp.render_to_string size t + BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size t let txt_of_cic_term size metasenv context t = let fake_sequent = (-1,context,t) in