X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.ml;h=d7e71177d5c524904548e6bb3a70d7a0d90ebde5;hb=95d791163d23738e82c4232598138f7cbab4207f;hp=5e75b5b2d9647d057f20e64aabbe1df031f1d516;hpb=2da9c5cef39f1512fc604adb30e9b0ecae4b2881;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 5e75b5b2d..d7e71177d 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -319,7 +319,7 @@ module Make(C:Callbacks) =
      match scratch_window#sequent_viewer#get_selected_terms with
         [] ->
          C.output_html
-          ("<h1 color=\"red\">No term selected</h1>")
+          ("<h1 color=\"red\">No terms selected</h1>")
       | terms ->
          try
           let expr = tactic terms scratch_window#term in