]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitacLib.ml
FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:
[helm.git] / helm / software / matita / matitacLib.ml
index 7580ebf2969545acb112ac0f2ca909bdc466feaa..c0c3d094188079b715766ca2ce61d3bb210efb37 100644 (file)
@@ -274,7 +274,7 @@ let compile atstart options fname =
         (* FG: we do not generate .moo when dumping .mma files *)
         GrafiteMarshal.save_moo moo_fname moo_content_rev;
         LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
-        NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri)
+        NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
          (GrafiteTypes.get_dump grafite_status)
      end;
      let tm = Unix.gmtime elapsed in