Some more datatypes lifted to Type.

[helm.git] / matita / applyTransformation.ml

diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index fe8d9e569d24a38a62c77b1d2bc1c1b310e62288..f27da2caa64d3765b76cffa30f2bf310def03a7e 100644 (file)
--- a/matita/applyTransformation.ml
+++ b/matita/applyTransformation.ml
@@ -70,6 +70,20 @@ let mml_of_cic_object obj =
    (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
   ids_to_inner_sorts,ids_to_inner_types)))
 
+let txt_of_cic_sequent size metasenv sequent =
+  let unsh_sequent,(asequent,ids_to_terms,
+    ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
+  =
+    Cic2acic.asequent_of_sequent metasenv sequent
+  in
+  let content_sequent = Acic2content.map_sequent asequent in 
+  let pres_sequent = 
+   CicNotationPres.mpres_of_box
+    (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
+  in
+  BoxPp.render_to_string (function x::_ -> x | _ -> assert false) size
+   pres_sequent
+
 let txt_of_cic_sequent_conclusion size metasenv sequent = 
   let _,(asequent,_,_,ids_to_inner_sorts,_) = 
     Cic2acic.asequent_of_sequent metasenv sequent 
@@ -78,9 +92,8 @@ 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
   txt_of_cic_sequent_conclusion size metasenv fake_sequent 
-