new tactics are almost ready

[helm.git] / helm / software / components / disambiguation / disambiguate.ml

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 44498d08830b5b7c266f5573739ef119cf772f43..fa63d1f484e6daca79d910587dafd579fcf5ed15 100644 (file)
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -409,7 +409,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 let disambiguate_thing 
   ~context ~metasenv ~subst ~use_coercions
   ~string_context_of_context
-  ~initial_ugraph:base_univ ~hint
+  ~initial_ugraph:base_univ ~expty
   ~mk_implicit ~description_of_alias
   ~aliases ~universe ~lookup_in_library 
   ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
@@ -489,14 +489,9 @@ let disambiguate_thing
          interpretate_thing ~context ~env:filled_env
           ~uri ~is_path:false thing ~localization_tbl
        in
-       let cic_thing = (fst hint) metasenv cic_thing in
 let foo () =
-       let k =
         refine_thing metasenv subst context uri
-         ~use_coercions cic_thing ugraph ~localization_tbl
-       in
-       let k = (snd hint) k in
-         k
+         ~use_coercions cic_thing expty ugraph ~localization_tbl
 in refine_profiler.HExtlib.profile foo ()
      with
      | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))