]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/applyTransformation.mli
hacks for paramodulation declarative proofs
[helm.git] / helm / software / matita / applyTransformation.mli
index 63c3beedf4a22225aea0f2680464b785901eabb1..170980cb0e2f95c87c39a02d58150b7f22ec1453 100644 (file)
@@ -68,7 +68,8 @@ val txt_of_cic_sequent_conclusion:
 (* columns, rendering style, name prefix, object *)
 val txt_of_cic_object: 
   ?map_unicode_to_tex:bool -> 
-  ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:bool ->  
+  ?skip_thm_and_qed:bool -> 
+  ?skip_initial_lambdas:bool -> 
     int -> GrafiteAst.presentation_style -> string ->
   Cic.obj ->
     string