abstracted pretty printers over inner pretty printing units (terms, lazy terms, and...

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

diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml
index 8b4f8858b8bf8f3b33b0b50f0670c1499d370d80..8c6928b7b6423b41e217c70074bd49322721ffd1 100644 (file)
--- a/helm/ocaml/grafite/grafiteMarshal.ml
+++ b/helm/ocaml/grafite/grafiteMarshal.ml
@@ -27,7 +27,7 @@ exception Checksum_failure of string
 exception Corrupt_moo of string
 exception Version_mismatch of string
 
-type ast_command = (Cic.term, Cic.obj) GrafiteAst.command
+type ast_command = Cic.obj GrafiteAst.command
 type moo = ast_command list
 
 let marshal_flags = []
@@ -50,13 +50,14 @@ let rehash_cmd_uris =
       in
       let appl_pattern = aux cic_appl_pattern in
       GrafiteAst.Interpretation (loc, dsc, args, appl_pattern)
-  | GrafiteAst.Coercion (loc, term, close) ->
-      GrafiteAst.Coercion (loc, CicUtil.rehash_term term, close)
+  | GrafiteAst.Coercion (loc, uri, close) ->
+      GrafiteAst.Coercion (loc, rehash_uri uri, close)
   | GrafiteAst.Notation _
   | GrafiteAst.Alias _ as cmd -> cmd
   | cmd ->
       prerr_endline "Found a command not expected in a .moo:";
-      prerr_endline (GrafiteAstPp.pp_cic_command cmd);
+      let obj_pp _ = assert false in
+      prerr_endline (GrafiteAstPp.pp_command ~obj_pp cmd);
       assert false
 
 (** .moo file format