X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=f3ba95765274fcd5788b1dad2112177fa9e49ba8;hb=847f57ed13f0b281dc3f2aa84bd89252d1b6a989;hp=348ca7c099fbacb707f8b84d55386573a2e746d3;hpb=e0378cef913a27d566b4159e4889f0fb82cee974;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 348ca7c09..f3ba95765 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -310,7 +310,9 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                 [] subst in
             [ Node ([loc], Id name, terms) ]))
   | Ast.Uri _ -> []
-  | Ast.Implicit -> []
+  | Ast.NRef _ -> []
+  | Ast.NCic _ -> []
+  | Ast.Implicit _ -> []
   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
   | Ast.Meta (index, local_context) ->
       List.fold_left
@@ -333,7 +335,7 @@ let domain_of_term ~context term =
 let domain_of_obj ~context ast =
  assert (context = []);
   match ast with
-   | Ast.Theorem (_,_,ty,bo) ->
+   | Ast.Theorem (_,_,ty,bo,_) ->
       domain_of_term [] ty
       @ (match bo with
           None -> []
@@ -409,7 +411,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 
@@ -443,10 +445,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> *)
@@ -492,14 +491,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))