The library is no longer automatically used during disambiguation.

[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 becf2a41229c18b0b3259a1f2d453a05d0e716c7..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);
   ]
 ;;