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 bfeb65d37ea2d39888abb3303026ead0ad5d62e7..352b043a4df4704ff8d6b288efbfca16ac77e418 100644 (file)
--- 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