From 7a974bd5775acf432e4074f32a99cc08d42b667f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 18 Oct 2006 17:39:48 +0000 Subject: [PATCH] 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. --- components/cic_disambiguation/disambiguate.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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 -- 2.39.2