Added new function txt_of_cic_sequent.

[helm.git] / helm / software / matita / applyTransformation.mli

diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli
index 8e2d51b5b6713e06ad4b9f1b04cfefb11552409e..218a92ca9f4d8bc0263f16c77cd6610e538c8ee4 100644 (file)
--- a/helm/software/matita/applyTransformation.mli
+++ b/helm/software/matita/applyTransformation.mli
@@ -57,6 +57,8 @@ val mml_of_cic_object:
 
 val txt_of_cic_term: 
   int -> Cic.metasenv -> Cic.context -> Cic.term -> string 
+val txt_of_cic_sequent: 
+  int -> Cic.metasenv -> Cic.conjecture -> string
 val txt_of_cic_sequent_conclusion: 
   int -> Cic.metasenv -> Cic.conjecture -> string