Objects are now used to represent also the tactic status.

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

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index cc46c76492e43218f24ed1779beb4b720711f78f..4bd7390f988c254d4de93874aa583daa74980686 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -111,7 +111,8 @@ let _ =
            ProofMode nstatus ->
             sequents_viewer#nload_sequents nstatus;
             (try
-              script#setGoal (Some (Continuationals.Stack.find_goal nstatus.NTacStatus.gstatus));
+              script#setGoal
+               (Some (Continuationals.Stack.find_goal nstatus#stack));
               let goal =
                match script#goal with
                   None -> assert false