Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:

take care of checking progress when solving the remaining problems, distinguishing between solved and stuck conversions.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15467 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 5 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e261438f8d..127e52e9a7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -821,12 +821,27 @@ let solve_unconstrained_impossible_cases evd =
 
 let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
   let evd = solve_unconstrained_evars_with_canditates evd in
-  let (evd,pbs) = extract_all_conv_pbs evd in
-  let heuristic_solved_evd = List.fold_left
-    (fun evd (pbty,env,t1,t2) ->
+  let rec aux evd pbs progress stuck =
+    match pbs with
+    | (pbty,env,t1,t2 as pb) :: pbs ->
       let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in
-	if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
-    evd pbs in
+	if b then 
+	  let (evd', rest) = extract_all_conv_pbs evd' in
+	    if rest = [] then aux evd' pbs true stuck
+	    else (* Unification got actually stuck, postpone *)
+	      aux evd pbs progress (pb :: stuck)
+	else Pretype_errors.error_cannot_unify env evd (t1, t2)
+    | _ -> 
+	if progress then aux evd stuck false []
+	else 
+	  match stuck with
+	  | [] -> (* We're finished *) evd
+	  | (pbty,env,t1,t2) :: _ ->
+	      (* There remains stuck problems *)
+	      Pretype_errors.error_cannot_unify env evd (t1, t2)
+  in
+  let (evd,pbs) = extract_all_conv_pbs evd in
+  let heuristic_solved_evd = aux evd pbs false [] in
   check_problems_are_solved env heuristic_solved_evd;
   solve_unconstrained_impossible_cases heuristic_solved_evd