From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 20 Apr 2004 17:00:53 +0000 (+0000)
Subject: got rid of a ~status label
X-Git-Tag: dead_dir_walking~22
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=947e7893dbb23fcaa998266ee8dd9a32b27d3b6e

got rid of a ~status label
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index b13555740..988eb7e14 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2076,7 +2076,7 @@ let searchPattern () =
       | Some metano ->
          let uris' =
            TacticChaser.matchConclusion mqi_handle
-            ~choose_must () ~status:(proof, metano)
+            ~choose_must () (proof, metano)
          in
          let uri' =
           user_uri_choice ~title:"Ambiguous input."