From: Claudio Sacerdoti Coen Date: Wed, 18 Oct 2006 14:13:25 +0000 (+0000) Subject: Bug fixed: the diff component of the exception raised when the term cannot X-Git-Tag: 0.4.95@7852~880 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a277e8ea1a71fe80b771650409cda5efdf47667c;p=helm.git 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. --- 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