- let choices =
- match item with
- | Id id ->
- (try
- Hashtbl.find id_choices id
- with Not_found ->
- let choices = choices_of_id dbd id in
- Hashtbl.add id_choices id choices;
- choices)
- | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
- | Num instance -> DisambiguateChoices.lookup_num_choices ()
- in
- if choices = [] then raise (No_choices item);
- choices
+ let choices =
+ let lookup_in_library () =
+ match item with
+ | Id id -> choices_of_id dbd id
+ | Symbol (symb, _) ->
+ List.map DisambiguateChoices.mk_choice
+ (CicNotationRew.lookup_interpretations symb)
+ | Num instance ->
+ DisambiguateChoices.lookup_num_choices ()
+ in
+ match universe with
+ | None -> lookup_in_library ()
+ | Some e ->
+ (try
+ Environment.find item e
+ with Not_found -> lookup_in_library ())
+ in
+ if choices = [] then raise (No_choices item);
+ choices