From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 30 Oct 2002 15:29:30 +0000 (+0000)
Subject: Minor interface improvement.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbb60b312f137979284cb123d17a0a0729bf3922;p=helm.git

Minor interface improvement.
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e5ad5973e..85f56c155 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1267,7 +1267,9 @@ let searchPattern rendering_window () =
             " <h1>Objects that can actually be applied: </h1> " ^
             String.concat "<br>" uris' ^ exc ^
             " <h1>Number of false matches: " ^
-             string_of_int (List.length uris - List.length uris') ^ "</h1>"
+             string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
+            " <h1>Number of good matches: " ^
+             string_of_int (List.length uris') ^ "</h1>"
            in
             output_html outputhtml html' ;
             let uri' = user_uri_choice uris' in