]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/disambiguate.ml
unification hints almost ready
[helm.git] / helm / software / components / disambiguation / disambiguate.ml
index 348ca7c099fbacb707f8b84d55386573a2e746d3..44498d08830b5b7c266f5573739ef119cf772f43 100644 (file)
@@ -443,10 +443,7 @@ let disambiguate_thing
               | item -> item
             in
             Environment.find item e
-          with Not_found -> 
-            lookup_in_library 
-              interactive_user_uri_choice 
-              input_or_locate_uri item)
+          with Not_found -> [])
    in
 (*
       (* <benchmark> *)