Fixing universe levels for saturations and (partially) basic_topologies.

[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 9415e3a744f2084b541cda0e69f0a3db2f898f01..63bcaa587197b08da14e9b211f2cb4688085016e 100644 (file)
--- 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