function to domp moo_content is now exported

[helm.git] / helm / matita / matitacLib.mli

diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli
index 8032320ce7103b487da2e048155ef9e631629d31..a053a3f1a1318dd0ab667877cbaf8df50b9a0e14 100644 (file)
--- a/helm/matita/matitacLib.mli
+++ b/helm/matita/matitacLib.mli
@@ -28,6 +28,7 @@ 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
 
 (** clean_exit n
   performs an exit [n] after a complete clean-up of what was partially compiled