From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 25 Nov 2005 16:33:25 +0000 (+0000)
Subject: bugfix: removed unneeded No_choices exception
X-Git-Tag: make_still_working~8097
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dd3b2ca095995254d43dd0b2d3d474428a007616;p=helm.git

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 3e6ce26e7..41025ee3a 100644
--- 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