Estatus finally merged into the global status using inheritance.

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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 18b406708bc8c64521b4d8132b96205bfa8ae5ca..36f7cda6dc9d059bb22a14324dfbdd3febdc00f5 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -235,8 +235,7 @@ let compile atstart options fname =
       with
       | [] -> grafite_status
       | (g,None)::_ -> g
-      | (g,Some _)::_ -> 
-            raise (AttemptToInsertAnAlias (GrafiteTypes.get_estatus g))
+      | (g,Some _)::_ -> raise (AttemptToInsertAnAlias g)
      with MatitaEngine.EnrichedWithStatus 
             (GrafiteEngine.Macro (floc, f), grafite) as exn ->
             match f (get_macro_context (Some grafite)) with 
@@ -258,7 +257,7 @@ let compile atstart options fname =
     let elapsed = Unix.time () -. time in
     let proof_status,moo_content_rev,lexicon_content_rev = 
       grafite_status#proof_status, grafite_status#moo_content_rev, 
-       (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev
+       grafite_status#lstatus.LexiconEngine.lexicon_content_rev
     in
     if proof_status <> GrafiteTypes.No_proof then
      (HLog.error
@@ -275,7 +274,7 @@ let compile atstart options fname =
         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)
-         (GrafiteTypes.get_estatus grafite_status)#dump
+         grafite_status#dump
      end;
      let tm = Unix.gmtime elapsed in
      let sec = string_of_int tm.Unix.tm_sec ^ "''" in