hSqlite3.ml used create_fun_2 to define REGEXP.

[helm.git] / matita / applyTransformation.mli

diff --git a/matita/applyTransformation.mli b/matita/applyTransformation.mli
index 2718d6401d37edafdf55dfdc5a057b1bfb3cd8c3..63c3beedf4a22225aea0f2680464b785901eabb1 100644 (file)
--- a/matita/applyTransformation.mli
+++ b/matita/applyTransformation.mli
@@ -67,7 +67,9 @@ 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