X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=f9c9af3590de8cdb03a1ba1f6dde67f4e7a18ef1;hb=56c4e355b88aa505b64c539053aba92eb86afc2a;hp=30c7fc9eaf954a9306d0c6c3c0b9884538aa4d85;hpb=9a7c77e5c29d764109a104aa629761ba90cb511c;p=helm.git

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index 30c7fc9ea..f9c9af359 100644
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -141,8 +141,7 @@ 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);
+            ~present:cur_grafite_status ~past:grafite_status;
            GrafiteSync.time_travel
             ~present:cur_grafite_status ~past:grafite_status;
            interactive_loop (Some n)
@@ -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