From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 18 Oct 2006 17:39:48 +0000 (+0000)
Subject: Missing optimization implemented: before starting to analyze the disambiguation
X-Git-Tag: 0.4.95@7852~878
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a974bd5775acf432e4074f32a99cc08d42b667f;p=helm.git

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/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 04357ef92..3f3d8235a 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/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