diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 20:55:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 20:55:31 +0000 |
| commit | 8e4b7319caa0754401c8b868e9ce9490a867d7f1 (patch) | |
| tree | efbb3e085ff7f28dc8310bc906189846f69cf32d /pretyping/evarconv.mli | |
| parent | a5808860fbabd1239d1116c2f4413d56ff99620f (diff) | |
Reverted commit r13893 about propagation of more informative
unification failure messages (it is not fully usable and was not
intended to be committed now, sorry for the noise).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index d2d74ff96..e1f507b0a 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -13,9 +13,7 @@ open Environ open Reductionops open Evd -exception NotUnifiable of evar_map * Pretype_errors.unification_error - -(** returns exception NotUnifiable with best known evar_map if not unifiable *) +(** returns exception Reduction.NotConvertible 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 +25,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 -> Evarutil.unification_result + env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool val evar_eqappr_x : transparent_state -> env -> evar_map -> conv_pb -> constr * constr list -> constr * constr list -> - Evarutil.unification_result + evar_map * bool (**/**) val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map |