From dd3b2ca095995254d43dd0b2d3d474428a007616 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 25 Nov 2005 16:33:25 +0000 Subject: [PATCH] bugfix: removed unneeded No_choices exception bugfix: avoid looking in the library when explecitely asked not to do so --- helm/ocaml/cic_disambiguation/disambiguate.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) 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 -- 2.39.2