]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitacLib.mli
- changed moo representation in MatitaTypes.status, no longer a string list, but...
[helm.git] / helm / matita / matitacLib.mli
index b19ff5b90c4ef0ef72ef09bc3d494452565960d3..7c07402d875f144ef99c9adfd182c2015f336353 100644 (file)
@@ -30,7 +30,10 @@ val go : unit -> unit
 val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit
 
 (** fname is the .ma *)
-val dump_moo_to_file: string -> string list -> unit
+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