X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2FmultiPassDisambiguator.ml;h=86d037742652c99085ff07092dceaf371447d5dd;hb=4e98c439731c6e110430a6c5217274215bf403b6;hp=9415e3a744f2084b541cda0e69f0a3db2f898f01;hpb=62f476a05884d451bfb90d845ea2b1c0a1c77f96;p=helm.git

diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml
index 9415e3a74..86d037742 100644
--- a/helm/software/components/disambiguation/multiPassDisambiguator.ml
+++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml
@@ -41,18 +41,21 @@ exception DisambiguationError of
 (* implement module's API *)
 
 let only_one_pass = ref false;;
+let use_library = ref false;;
 
 let passes () = (* <fresh_instances?, aliases, coercions?> *)
  if !only_one_pass then
   [ (true, `Mono, false) ]
+ else if !use_library then
+  [ (true, `Library, false); 
+      (* for demo to reduce the number of interpretations *)
+    (true, `Library, true);
+  ]
  else
   [ (true, `Mono, false);
     (true, `Multi, false);
     (true, `Mono, true);
     (true, `Multi, true);
-    (true, `Library, false); 
-      (* for demo to reduce the number of interpretations *)
-    (true, `Library, true);
   ]
 ;;
 
@@ -124,7 +127,6 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
   in
   let rec aux i errors passes =
   debug_print (lazy ("Pass: " ^ string_of_int i));
-  prerr_endline (("Pass: " ^ string_of_int i));
    match passes with
       [ pass ] ->
         (try
@@ -141,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
  =
@@ -149,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)