More statuses converted to objects.

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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index baac2409cf1a3243cd5833ffb7ddd81091bf7061..18b406708bc8c64521b4d8132b96205bfa8ae5ca 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -99,7 +99,7 @@ let dump f =
 ;;
 
 let get_macro_context = function
-   | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
+   | Some status when status#proof_status = GrafiteTypes.No_proof -> []
    | Some status                ->
       let stack = GrafiteTypes.get_stack status in
       let goal = Continuationals.Stack.find_goal stack in
@@ -257,7 +257,7 @@ let compile atstart options fname =
     in
     let elapsed = Unix.time () -. time in
     let proof_status,moo_content_rev,lexicon_content_rev = 
-      grafite_status.proof_status, grafite_status.moo_content_rev, 
+      grafite_status#proof_status, grafite_status#moo_content_rev, 
        (GrafiteTypes.get_estatus grafite_status)#lstatus.LexiconEngine.lexicon_content_rev
     in
     if proof_status <> GrafiteTypes.No_proof then