Disambiguation can now return more than one choice.

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index f3690204f2cee7218b9902a363e56ee5948cdc55..2d8a7067c5fbe5e4edcd2df82ee1a0c7c7a1b43e 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -472,8 +472,12 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id
         in
         let module Disambiguate' = DisambiguatingParser.Make(Chat) in
         let (id_to_uris', metasenv', term') =
+         match
           Disambiguate'.disambiguate_term mqi_handle
             context metasenv term_string id_to_uris
+         with
+            [id_to_uris',metasenv',term'] -> id_to_uris',metasenv',term'
+          | _ -> assert false
         in
         (match metasenv' with
         | [] ->