diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ed087fa25..0321707b0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -650,7 +650,8 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function 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 else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") @@ -662,7 +663,8 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function try ignore (Nativeconv.native_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 else user_err_loc (loc,"",str "Cannot check cast with native compiler: " ++ str "unresolved arguments remain.") |