diff options
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 e1f507b0a..d2d74ff96 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 |