removed no longer used METAs

[helm.git] / helm / ocaml / grafite / grafiteMarshal.mli

diff --git a/helm/ocaml/grafite/grafiteMarshal.mli b/helm/ocaml/grafite/grafiteMarshal.mli
index 663d2fa43c0a00d1852166d2da42ce1a7392b722..e60ad39d8daa370ee9c4fdd21bcbf9f564e710ad 100644 (file)
--- a/helm/ocaml/grafite/grafiteMarshal.mli
+++ b/helm/ocaml/grafite/grafiteMarshal.mli
@@ -23,13 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
-  (** name of the corrupt .moo file *)
-exception Checksum_failure of string
-exception Corrupt_moo of string
-exception Version_mismatch of string
-
-type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
-type moo = ast_command list * GrafiteAst.metadata list  (** <moo, metadata> *)
+type ast_command = Cic.obj GrafiteAst.command
+type moo = ast_command list
 
 val save_moo: fname:string -> moo -> unit