diff options
| author | herbelin | 2011-03-07 20:11:32 +0000 |
|---|---|---|
| committer | herbelin | 2011-03-07 20:11:32 +0000 |
| commit | 6cbd65aa4e5fe82259b44b89e5e624ed2299249c (patch) | |
| tree | ee4b6d9b9430519bfc153a405e88edc9b2ced2e7 /pretyping/unification.ml | |
| parent | 0176dd0d2d657867c7ecc93fc979dc15c1409336 (diff) | |
Added propagation of evars unification failure reasons for better
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
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 6121ba7d87..6e39d9831c 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] |