]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite/grafiteMarshal.mli
added default for matita.noiinertypes
[helm.git] / components / grafite / grafiteMarshal.mli
index e60ad39d8daa370ee9c4fdd21bcbf9f564e710ad..cad7b1187a62869f25ff4d15aa63ca81e1770303 100644 (file)
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-type ast_command = Cic.obj GrafiteAst.command
+type ast_command = (Cic.term,Cic.obj) GrafiteAst.command
 type moo = ast_command list
 
 val save_moo: fname:string -> moo -> unit