diff options
| author | herbelin | 2013-02-17 14:56:11 +0000 |
|---|---|---|
| committer | herbelin | 2013-02-17 14:56:11 +0000 |
| commit | f5e644a53c69392f94eae01dd71ab79b4700a892 (patch) | |
| tree | 592ea17a9580bede8e1aa7dc6dbd878e4e190e63 /pretyping/unification.ml | |
| parent | 358c68e60a4a82dbce209559b94858e917590787 (diff) | |
A more informative message when the elimination predicate for
destruct, rewrite, etc. is not well-typed.
Also added support for a more informative message when the elimination
predicate is not well-formed while using the smart "second-order"
unification algorithm. However the "abstract_list_all" algorithm seems
to remain more informative though, so we still use this algorithm for
reporting about ill-typed predicates.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 4c0f12d3c7..8b89bd438d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -69,8 +69,11 @@ let abstract_list_all env evd typ c l = let p = abstract_scheme env c l_with_all_occs ctxt in let typp = try Typing.type_of env evd p - with UserError _ | Type_errors.TypeError _ -> - error_cannot_find_well_typed_abstraction env evd p l in + with + | UserError _ -> + error_cannot_find_well_typed_abstraction env evd p l None + | Type_errors.TypeError (env',x) -> + error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in (p,typp) let set_occurrences_of_last_arg args = @@ -83,8 +86,8 @@ let abstract_list_all_with_dependencies env evd typ c l = let evd,b = Evarconv.second_order_matching empty_transparent_state env evd ev' argoccs c in - if b then nf_evar evd (existential_value evd (destEvar ev)) - else error "Cannot find a well-typed abstraction." + let p = nf_evar evd (existential_value evd (destEvar ev)) in + if b then p else error_cannot_find_well_typed_abstraction env evd p l None (**) |