From 8ac929ea128f1f7353b3f4d532b642e769542e55 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 17 Feb 2013 14:56:04 +0000 Subject: 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@16205 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarconv.mli | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'pretyping/evarconv.mli') diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 285c509f1..d3f8b451a 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -15,7 +15,9 @@ open Reductionops open Evd open Locus -(** returns exception Reduction.NotConvertible if not unifiable *) +exception UnableToUnify 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 @@ -27,11 +29,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 -> Evarsolve.unification_result val evar_eqappr_x : transparent_state -> env -> evar_map -> conv_pb -> constr * constr stack -> constr * constr stack -> - evar_map * bool + Evarsolve.unification_result (**/**) val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map -- cgit v1.2.3