diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 20:11:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 20:11:32 +0000 |
| commit | 6cbd65aa4e5fe82259b44b89e5e624ed2299249c (patch) | |
| tree | ee4b6d9b9430519bfc153a405e88edc9b2ced2e7 /pretyping/evarutil.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/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index a4c07a019..705ab356f 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -74,13 +74,20 @@ val whd_head_evar : evar_map -> constr -> constr val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool val solve_refl : - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) + (env -> evar_map -> conv_pb -> constr -> constr -> bool) -> env -> evar_map -> existential_key -> constr array -> constr array -> evar_map + +type unification_result = + | Success of evar_map + | UnifFailure of evar_map * Pretype_errors.unification_error + +val is_success : unification_result -> bool + val solve_simple_eqn : - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) + (env -> evar_map -> conv_pb -> constr -> constr -> unification_result) -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> - evar_map * bool + unification_result (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) |