diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 12 |
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 |