fixed a finalization issue for connections closed twice

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

diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli
index 8032320ce7103b487da2e048155ef9e631629d31..7c07402d875f144ef99c9adfd182c2015f336353 100644 (file)
--- a/helm/matita/matitacLib.mli
+++ b/helm/matita/matitacLib.mli
@@ -29,7 +29,15 @@ val interactive_loop : unit -> unit
 val go : unit -> unit
 val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit
 
+(** fname is the .ma *)
+val dump_moo_to_file:
+  string ->
+  (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list ->
+    unit
+
 (** clean_exit n
-  performs an exit [n] after a complete clean-up of what was partially compiled
+  if n = Some n it performs an exit [n] after a complete clean-up of what was
+   partially compiled
+  otherwise it performs the clean-up without exiting
 *)
-val clean_exit : int -> unit
+val clean_exit : int option -> unit