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 3f3d8235aa79730fbb850c8cb3fd93303e398097..1560f00160247992ab701c0e1f2243d49ffcd5ab 100644 (file)
--- 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