diff options
| author | herbelin | 2011-03-07 20:11:32 +0000 |
|---|---|---|
| committer | herbelin | 2011-03-07 20:11:32 +0000 |
| commit | 6cbd65aa4e5fe82259b44b89e5e624ed2299249c (patch) | |
| tree | ee4b6d9b9430519bfc153a405e88edc9b2ced2e7 /pretyping/pretyping.ml | |
| 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/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1ea2dbd002..003f507dcf 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -640,7 +640,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct try ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj with Reduction.NotConvertible -> - error_actual_type_loc loc env !evdref cj tval + error_actual_type_loc loc env !evdref cj tval + (ConversionFailed (env,cty,tval)) end | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval) in |