Fixed a call to auto, and commented the remaining part.

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 04357ef92ac1e3e3e52ca48b461ecfcdaad2b662..f3600b7cbc34602ba9e8a433ae853aaf66f4d3b8 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/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
@@ -1019,10 +1022,16 @@ in refine_profiler.HExtlib.profile foo ()
                in
                 filter base_univ choices
       in
+      let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
+       match test_env aliases todo_dom base_univ with
+        | Ok _,_
+        | Uncertain _,_ ->
+           aux aliases diff lookup_in_todo_dom todo_dom base_univ
+        | Ko (loc,msg),_ -> ([],[aliases,diff,loc,msg]) in
       let base_univ = initial_ugraph in
       try
         let res =
-         match aux aliases [] None todo_dom base_univ with
+         match aux' aliases [] None todo_dom base_univ with
          | [],errors ->
             let errors =
              List.map