Useless code removed.

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

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index eb39e019ddfc54472aa457d0eedb648adc8dd42c..680dec8e612850447ca1f179bb1e9a48dd6c19d3 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -1005,15 +1005,11 @@ class gui () =
              `ProofMode ->
               sequents_viewer#nload_sequents grafite_status;
               (try
-                script#setGoal
-                 (Some (Continuationals.Stack.find_goal grafite_status#stack));
                 let goal =
-                 match script#goal with
-                    None -> assert false
-                  | Some n -> n
+                 Continuationals.Stack.find_goal grafite_status#stack
                 in
                  sequents_viewer#goto_sequent grafite_status goal
-              with Failure _ -> script#setGoal None);
+              with Failure _ -> ());
            | `CommandMode -> sequents_viewer#load_logo
         in
         script#addObserver sequents_observer;