]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/applyTransformation.ml
Added lt_O_S.
[helm.git] / matita / applyTransformation.ml
index fe8d9e569d24a38a62c77b1d2bc1c1b310e62288..6e92cfa95a43fbfc35acf6f01eb622d560286fee 100644 (file)
@@ -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