X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=fe8d9e569d24a38a62c77b1d2bc1c1b310e62288;hb=21f2ca1e83578359d9ab6926d466a4645049ee76;hp=83e5f3c18e42dd97a04222180ddb57f5bc1684a2;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 83e5f3c18..fe8d9e569 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -70,3 +70,17 @@ 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_conclusion size metasenv sequent = 
+  let _,(asequent,_,_,ids_to_inner_sorts,_) = 
+    Cic2acic.asequent_of_sequent metasenv sequent 
+  in
+  let _,_,_,t = Acic2content.map_sequent asequent in 
+  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
+
+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 
+