1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way,

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

diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml
index 63bcaa587197b08da14e9b211f2cb4688085016e..5767aa3e3f04f09564beb9aa1d70d64f846f9335 100644 (file)
--- a/helm/software/components/disambiguation/multiPassDisambiguator.ml
+++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml
@@ -27,9 +27,9 @@
 
 open Printf
 
-let debug = false;;
+let debug = ref false;;
 let debug_print s =
- if debug then prerr_endline (Lazy.force s);;
+ if !debug then prerr_endline (Lazy.force s) else ();;
 
 exception DisambiguationError of
  int *
@@ -143,7 +143,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
    aux 1 [] passes
 
 let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
-  ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit
+  ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit
   ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing
   ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing
  =
@@ -151,7 +151,7 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
     let thing = if fresh_instances then freshen_thing thing else thing in
      Disambiguate.disambiguate_thing
       ~context ~metasenv ~subst ~use_coercions ~string_context_of_context
-      ~initial_ugraph ~hint ~mk_implicit ~description_of_alias
+      ~initial_ugraph ~expty ~mk_implicit ~description_of_alias
       ~aliases ~universe ~lookup_in_library 
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
       ~mk_localization_tbl (txt,len,thing)