From: Claudio Sacerdoti Coen Date: Fri, 31 Jan 2003 18:45:15 +0000 (+0000) Subject: ... X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=95d791163d23738e82c4232598138f7cbab4207f ... --- 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 - ("

No term selected

") + ("

No terms selected

") | terms -> try let expr = tactic terms scratch_window#term in