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 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 |