]> matita.cs.unibo.it Git - helm.git/commitdiff
got rid of a ~status label
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 20 Apr 2004 17:00:53 +0000 (17:00 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 20 Apr 2004 17:00:53 +0000 (17:00 +0000)
helm/gTopLevel/gTopLevel.ml

index b13555740e9086724345aa3def6df0c8c1ccb9fd..988eb7e143e9a86ba563095a7dac0f4294976904 100644 (file)
@@ -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."