diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 913e80f39..98dea9fc9 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -412,7 +412,7 @@ let inh_tosort_force loc env evd j = let j2 = on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env j2) with Not_found | NoCoercion -> - error_not_a_type_loc loc env evd j + error_not_a_type ~loc env evd j let inh_coerce_to_sort loc env evd j = let typ = whd_all env evd j.uj_type in @@ -506,16 +506,16 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> - error_actual_type_loc loc env best_failed_evd cj t e + error_actual_type ~loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in try if evd' == evd then - error_actual_type_loc loc env best_failed_evd cj t e + error_actual_type ~loc env best_failed_evd cj t e else inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (_evd,_error) -> - error_actual_type_loc loc env best_failed_evd cj t e + error_actual_type ~loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) |