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/evarconv.mli | |
| 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/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index e1f507b0ac..d2d74ff962 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -13,7 +13,9 @@ open Environ open Reductionops open Evd -(** returns exception Reduction.NotConvertible if not unifiable *) +exception NotUnifiable of evar_map * Pretype_errors.unification_error + +(** returns exception NotUnifiable with best known evar_map if not unifiable *) val the_conv_x : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map @@ -25,11 +27,11 @@ val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr - (**/**) (* For debugging *) val evar_conv_x : transparent_state -> - env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool + env -> evar_map -> conv_pb -> constr -> constr -> Evarutil.unification_result val evar_eqappr_x : transparent_state -> env -> evar_map -> conv_pb -> constr * constr list -> constr * constr list -> - evar_map * bool + Evarutil.unification_result (**/**) val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map |