Missing optimization implemented: before starting to analyze the disambiguation

domain we try first without interpreting any symbol. This way we can avoid
lot of refinements when the information in the uninterpreted term already
tells us that every instance will not be well typed.

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 04357ef92ac1e3e3e52ca48b461ecfcdaad2b662..3f3d8235aa79730fbb850c8cb3fd93303e398097 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -1019,10 +1019,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