The logo is now showed in the sequents_viewer window when there is no proof

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 610f22a4ec7943d6b3b53e7117fb10e9b5b1958b..72dff80581b73e641240e364384684bab9f1c37a 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -93,9 +93,9 @@ let _ =
         sequents_viewer#load_sequents status;
         sequents_viewer#goto_sequent goal
     | Proof proof -> 
-        prerr_endline "sequents_viewer#load_logo_with_qed (no proof)"; ()
+        sequents_viewer#load_logo_with_qed
     | No_proof -> 
-        prerr_endline "sequents_viewer#load_logo (no proof)"; ()
+        sequents_viewer#load_logo
     | Intermediate _ -> 
         assert false (* only the engine may be in this state *)
   in