]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitaWiki.ml
Initial implementation of statuses using objects in place of nested records.
[helm.git] / helm / software / matita / matitaWiki.ml
index eb115636f8360c07a461c39d4d10c25e38f847ec..7575eca10e3069b9a049531c54ab875cbfee5217 100644 (file)
@@ -227,7 +227,7 @@ let main () =
       |  s::_ ->
          s.proof_status, s.moo_content_rev,
           (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev,
-          GrafiteTypes.get_dump s
+          (GrafiteTypes.get_dstatus s)#dump
       | _ -> assert false
     in
     if proof_status <> GrafiteTypes.No_proof then
@@ -254,7 +254,7 @@ let main () =
        in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
-       NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
+       NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
        exit 0
      end
   with