X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FgTopLevel.ml;h=988eb7e143e9a86ba563095a7dac0f4294976904;hb=947e7893dbb23fcaa998266ee8dd9a32b27d3b6e;hp=b13555740e9086724345aa3def6df0c8c1ccb9fd;hpb=9e7e14a98d5b6c728f980979f21d542d829d9b98;p=helm.git

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."