bugfix: removed unneeded No_choices exception

bugfix: avoid looking in the library when explecitely asked not to do so

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 3e6ce26e7c5a56971cd6e1369b516b0eb7daba16..41025ee3a84e4e427827092331466365cee4c7d9 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -28,7 +28,6 @@ open Printf
 open DisambiguateTypes
 open UriManager
 
-exception No_choices of domain_item
 exception NoWellTypedInterpretation of string Lazy.t list
 exception PathNotWellFormed
 
@@ -760,10 +759,14 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
             | None -> lookup_in_library ()
             | Some e ->
                 (try
+                  let item =
+                    match item with
+                    | Symbol (symb, _) -> Symbol (symb, 0)
+                    | item -> item
+                  in
                   Environment.find item e
-                with Not_found -> lookup_in_library ())
+                with Not_found -> [])
           in
-          if choices = [] then raise (No_choices item);
           choices
       in
 (*
@@ -835,7 +838,7 @@ in refine_profiler.HExtlib.profile foo ()
                 None -> lookup_choices item
               | Some choices -> choices in
             match choices with
-               [] -> [], [lazy "No choices"]
+               [] -> [], [lazy ("No choices for " ^ string_of_domain_item item)]
              | [codomain_item] ->
                  (* just one choice. We perform a one-step look-up and
                     if the next set of choices is also a singleton we