updating the structures for sorts

[helm.git] / helm / software / matita / matitaWiki.ml

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index 30c7fc9eaf954a9306d0c6c3c0b9884538aa4d85..52d18f42a3ea5d43caaf6856d02d5aabb8377900 100644 (file)
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -141,10 +141,9 @@ let rec interactive_loop () =
           grafite_status := drop (to_be_dropped, !grafite_status) ;
           let grafite_status = safe_hd !grafite_status in
            LexiconSync.time_travel
-            ~present:(GrafiteTypes.get_estatus cur_grafite_status)
-            ~past:(GrafiteTypes.get_estatus grafite_status);
-           GrafiteSync.time_travel
             ~present:cur_grafite_status ~past:grafite_status;
+           GrafiteSync.time_travel
+            ~present:cur_grafite_status ~past:grafite_status ();
            interactive_loop (Some n)
     | `Do command ->
         let str = Ulexing.from_utf8_string command in
@@ -226,8 +225,7 @@ let main () =
       match !grafite_status with
       |  s::_ ->
          s#proof_status, s#moo_content_rev,
-          (GrafiteTypes.get_estatus s)#lstatus.LexiconEngine.lexicon_content_rev,
-          (GrafiteTypes.get_estatus s)#dump
+          s#lstatus.LexiconEngine.lexicon_content_rev, s#dump
       | _ -> assert false
     in
     if proof_status <> GrafiteTypes.No_proof then
@@ -253,7 +251,7 @@ let main () =
        in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
-       NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
+       NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
        exit 0
      end
   with