diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 7d480b8d48..13676b674c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -227,13 +227,20 @@ 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 = (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 |