Merge remote-tracking branch 'origin/matita-lablgtk3'

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

diff --git a/matita/components/disambiguation/multiPassDisambiguator.ml b/matita/components/disambiguation/multiPassDisambiguator.ml
index d3250c2fe144b911fb3f43778db785d57bec23f0..1ee9df14e8c7efdecfec04f3f20a9b9b8cf0492a 100644 (file)
--- a/matita/components/disambiguation/multiPassDisambiguator.ml
+++ b/matita/components/disambiguation/multiPassDisambiguator.ml
@@ -25,8 +25,6 @@
 
 (* $Id$ *)
 
-open Printf
-
 let debug = ref false;;
 let debug_print s =
  if !debug then prerr_endline (Lazy.force s) else ();;
@@ -51,6 +49,8 @@ let passes () = (* <fresh_instances?, aliases, coercions?> *)
       (* for demo to reduce the number of interpretations *)
     (true, `Library, true);
   ]
+ else if !debug then
+  [ (true, `Multi, true); ]
  else
   [ (true, `Mono, false);
     (true, `Multi, false);
@@ -117,7 +117,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
   let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
     f ~fresh_instances ~aliases ~universe ~use_coercions thing
   in
-  let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+  let set_aliases (_instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
    if use_mono_aliases then
     drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *)
    else if user_asked then