From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 30 Oct 2006 18:10:25 +0000 (+0000)
Subject: TermAcicContent.Interpretation_not_found catched and handled correctly.
X-Git-Tag: make_still_working~6692
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a7ffe734ba6742ff7a8cc2adcc43f17939390410;p=helm.git

TermAcicContent.Interpretation_not_found catched and handled correctly.
---

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 3f3d8235a..1560f0016 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -866,8 +866,11 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
               match item with
               | Id id -> choices_of_id dbd id
               | Symbol (symb, _) ->
-                  List.map DisambiguateChoices.mk_choice
+                 (try
+                   List.map DisambiguateChoices.mk_choice
                     (TermAcicContent.lookup_interpretations symb)
+                  with
+                   TermAcicContent.Interpretation_not_found -> [])
               | Num instance ->
                   DisambiguateChoices.lookup_num_choices ()
             in