X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_disambiguation%2Fdisambiguate.ml;h=f3600b7cbc34602ba9e8a433ae853aaf66f4d3b8;hb=70c533b5592b0bb91f544fec275213b866bf33ea;hp=3f3d8235aa79730fbb850c8cb3fd93303e398097;hpb=7a974bd5775acf432e4074f32a99cc08d42b667f;p=helm.git

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 3f3d8235a..f3600b7cb 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -727,12 +727,12 @@ let domain_of_obj ~context ast =
        List.flatten
         (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in
       let dom =
-       List.fold_left
-        (fun dom (_,ty) ->
+       List.fold_right
+        (fun (_,ty) dom ->
           match ty with
              None -> dom
-           | Some ty -> domain_rev_of_term [] ty @ dom
-        ) (dom @ domain_rev_of_term [] ty) params
+           | Some ty -> dom @ domain_rev_of_term [] ty
+        ) params (dom @ domain_rev_of_term [] ty)
       in
        List.filter
         (fun (_,name) ->
@@ -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