From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 8 Mar 2004 16:39:56 +0000 (+0000)
Subject: Disambiguation can now return more than one choice.
X-Git-Tag: v0_0_4~33
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8751721d61afcf2da67cb2ebdd70bb3e07aba551;p=helm.git

Disambiguation can now return more than one choice.
---

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index f3690204f..2d8a7067c 100644
--- 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
         | [] ->