X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteMarshal.ml;h=d18ee2f0c894fd12396067e80be1ec09c21cde05;hb=b108ab28153129d6578d7d9c2ffdf19e6779d86f;hp=15e4f5217cf054dc0e93995d71fc009a66546ecd;hpb=c3b7b4c8697a146a3d734b5333d655a25a642cb9;p=helm.git

diff --git a/matita/components/grafite/grafiteMarshal.ml b/matita/components/grafite/grafiteMarshal.ml
index 15e4f5217..d18ee2f0c 100644
--- a/matita/components/grafite/grafiteMarshal.ml
+++ b/matita/components/grafite/grafiteMarshal.ml
@@ -25,7 +25,7 @@
 
 (* $Id$ *)
 
-type ast_command = (Cic.term,Cic.obj) GrafiteAst.command
+type ast_command = GrafiteAst.command
 type moo = ast_command list
 
 let format_name = "grafite"
@@ -38,18 +38,13 @@ let load_moo_from_file ~fname =
   (raw: moo)
 
 let rehash_cmd_uris =
-  let rehash_uri uri =
-    UriManager.uri_of_string (UriManager.string_of_uri uri) in
   function
-  | GrafiteAst.Default (loc, name, uris) ->
-      let uris = List.map rehash_uri uris in
-      GrafiteAst.Default (loc, name, uris)
   | GrafiteAst.Include _ as cmd -> cmd
   | cmd ->
       prerr_endline "Found a command not expected in a .moo:";
       let term_pp _ = assert false in
       let obj_pp _ = assert false in
-      prerr_endline (GrafiteAstPp.pp_command ~term_pp ~obj_pp cmd);
+      prerr_endline (GrafiteAstPp.pp_command cmd);
       assert false
 
 let save_moo ~fname moo = save_moo_to_file ~fname (List.rev moo)