Estatus finally merged into the global status using inheritance.

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

diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index 30c7fc9eaf954a9306d0c6c3c0b9884538aa4d85..f9c9af3590de8cdb03a1ba1f6dde67f4e7a18ef1 100644 (file)
--- 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