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/evarconv.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/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c2ded73ad1..be5eb5dbdd 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -651,6 +651,8 @@ let set_solve_evars f = solve_evars := f * proposition from Dan Grayson] *) +exception TypingFailed of evar_map + let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = try let args = Array.to_list args in @@ -702,10 +704,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* We instantiate the evars of which the value is forced by typing *) let evd,rhs = - try !solve_evars env_evar evd rhs + let evdref = ref evd in + try let c = !solve_evars env_evar evdref rhs in !evdref,c with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) - raise Exit in + raise (TypingFailed !evdref) in let rec abstract_free_holes evd = function | (id,idty,c,_,evsref,_,_)::l -> @@ -736,7 +739,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = Evd.define evk rhs evd in abstract_free_holes evd subst, true - with Exit -> evd, false + with TypingFailed evd -> Evd.define evk rhs evd, false let second_order_matching_with_args ts env evd ev l t = (* |