X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.mli;h=7c07402d875f144ef99c9adfd182c2015f336353;hb=1946ca7a51df0acb35d8e2ea001d194f1d2ccb12;hp=dc24825e583a60e58ed89e642f094e3b57bd5591;hpb=5228acfa3e0e37019dac156ba85434b83e8f469d;p=helm.git

diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli
index dc24825e5..7c07402d8 100644
--- a/helm/matita/matitacLib.mli
+++ b/helm/matita/matitacLib.mli
@@ -28,7 +28,12 @@ val interactive_loop : unit -> unit
 (** go initializes the status and calls interactive_loop *)
 val go : unit -> unit
 val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit
-val dump_moo_to_file: string -> string list -> unit
+
+(** fname is the .ma *)
+val dump_moo_to_file:
+  string ->
+  (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list ->
+    unit
 
 (** clean_exit n
   if n = Some n it performs an exit [n] after a complete clean-up of what was