X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.mli;h=636c51d5754beddf21bf73ec9d7e298254cc2993;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7c07402d875f144ef99c9adfd182c2015f336353;hpb=f2551cc0cc563b34b88a70a6bb0ef5e352a5d542;p=helm.git

diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli
index 7c07402d8..636c51d57 100644
--- a/helm/matita/matitacLib.mli
+++ b/helm/matita/matitacLib.mli
@@ -29,12 +29,6 @@ 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
   if n = Some n it performs an exit [n] after a complete clean-up of what was
    partially compiled