hacks for paramodulation declarative proofs

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

diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli
index 2718d6401d37edafdf55dfdc5a057b1bfb3cd8c3..170980cb0e2f95c87c39a02d58150b7f22ec1453 100644 (file)
--- a/helm/software/matita/applyTransformation.mli
+++ b/helm/software/matita/applyTransformation.mli
@@ -67,7 +67,10 @@ val txt_of_cic_sequent_conclusion:
 
 (* columns, rendering style, name prefix, object *)
 val txt_of_cic_object: 
-  ?map_unicode_to_tex:bool -> int -> GrafiteAst.presentation_style -> string ->
+  ?map_unicode_to_tex:bool -> 
+  ?skip_thm_and_qed:bool -> 
+  ?skip_initial_lambdas:bool -> 
+    int -> GrafiteAst.presentation_style -> string ->
   Cic.obj ->
     string