From a277e8ea1a71fe80b771650409cda5efdf47667c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 18 Oct 2006 14:13:25 +0000 Subject: [PATCH] Bug fixed: the diff component of the exception raised when the term cannot be disambiguated used to lack the last choice in case of the look-ahead optimization. --- components/cic_disambiguation/disambiguate.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index bfeb65d37..352b043a4 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/components/cic_disambiguation/disambiguate.ml @@ -986,11 +986,11 @@ in refine_profiler.HExtlib.profile foo () remaining_dom new_univ) | Uncertain (loc,msg),new_univ -> (match remaining_dom with - | [] -> [], [diff,loc,msg] + | [] -> [], [new_diff,loc,msg] | _ -> aux new_env new_diff lookup_in_todo_dom remaining_dom new_univ) - | Ko (loc,msg),_ -> [], [diff,loc,msg]) + | Ko (loc,msg),_ -> [], [new_diff,loc,msg]) | _::_ -> let rec filter univ = function | [] -> [],[] @@ -1007,11 +1007,11 @@ in refine_profiler.HExtlib.profile foo () filter univ tl | Uncertain (loc,msg),new_univ -> (match remaining_dom with - | [] -> [],[diff,loc,msg] + | [] -> [],[new_diff,loc,msg] | _ -> aux new_env new_diff None remaining_dom new_univ ) @@ filter univ tl - | Ko (loc,msg),_ -> ([],[diff,loc,msg]) @@ filter univ tl) + | Ko (loc,msg),_ -> ([],[new_diff,loc,msg]) @@ filter univ tl) in filter base_univ choices in -- 2.39.2