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: 0.4.95@7852~833
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=406eaf99796e08d940cf24dafa3afa5679a8ba8b;p=helm.git

TermAcicContent.Interpretation_not_found catched and handled correctly.
---

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 3f3d8235a..1560f0016 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/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