Merge PR #7361: Towards selecting "best" unification failure among several

1 files changed, 11 insertions, 1 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 7d480b8d48..e978adf761 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -227,13 +227,23 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
 
+let join_failures evd1 evd2 e1 e2 =
+  match e1, e2 with
+  | _, CannotSolveConstraint (_,ProblemBeyondCapabilities) -> (evd1,e1)
+  | _ -> (evd2,e2)
+
 let rec ise_try evd = function
     [] -> assert false
   | [f] -> f evd
   | f1::l ->
       match f1 evd with
       | Success _ as x -> x
-      | UnifFailure _ -> ise_try evd l
+      | UnifFailure (evd1,e1) ->
+          match ise_try evd l with
+          | Success _ as x -> x
+          | UnifFailure (evd2,e2) ->
+              let evd,e = join_failures evd1 evd2 e1 e2 in
+              UnifFailure (evd,e)
 
 let ise_and evd l =
   let rec ise_and i = function