diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6121ba7d8..6e39d9831 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -638,9 +638,11 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) let solve_simple_evar_eqn ts env evd ev rhs = - let evd,b = solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) in - if not b then error_cannot_unify env evd (mkEvar ev,rhs); - Evarconv.consider_remaining_unif_problems env evd + match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with + | UnifFailure (evd,reason) -> + error_cannot_unify env evd ~reason (mkEvar ev,rhs); + | Success evd -> + Evarconv.consider_remaining_unif_problems env evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] |