]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite/grafiteMarshal.mli
1. matitaEngine splitted into disambiguation (now in grafite_parser) and
[helm.git] / helm / ocaml / grafite / grafiteMarshal.mli
index 663d2fa43c0a00d1852166d2da42ce1a7392b722..8fb1b23988c931e3121a8960e604715ddc2178f9 100644 (file)
@@ -28,7 +28,7 @@ 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 ast_command = (Cic.term, Cic.obj) GrafiteAst.command
 type moo = ast_command list * GrafiteAst.metadata list  (** <moo, metadata> *)
 
 val save_moo: fname:string -> moo -> unit