diff options
| author | Hugo Herbelin | 2018-04-26 15:51:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 14:21:10 +0200 |
| commit | 8ef1be1aead0dbcc2d3cc46a7e5eaa02f9ad6069 (patch) | |
| tree | 60e562a2662a8a499c359c2454a37425d217b1c7 /pretyping | |
| parent | cfefed1cb20b6abe33c222df49d346867bafbc7f (diff) | |
Unification failure: don't give preference to a "beyond capabilities" error.
This is actually a bit ad hoc at this stage in the sense that this is
specifically to prefer an informative first-order unification failure
over the currently always uninformative failure coming from
second-order unification.
When second-order unification shall be able to give more information,
one may consider alternative strategies, even maybe reporting not just
one but the list of failures in all (interesting) branches.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 13676b674c..e978adf761 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -227,7 +227,10 @@ 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 join_failures evd1 evd2 e1 e2 = + match e1, e2 with + | _, CannotSolveConstraint (_,ProblemBeyondCapabilities) -> (evd1,e1) + | _ -> (evd2,e2) let rec ise_try evd = function [] -> assert false |