diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 14:56:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 15:41:16 +0200 |
| commit | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch) | |
| tree | f76fd37023c71c20520e34e4a51c487e7a0388a0 /pretyping/coercion.ml | |
| parent | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff) | |
| parent | fc579fdc83b751a44a18d2373e86ab38806e7306 (diff) | |
Merge PR #244.
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 553786f58..2b860ae9c 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -411,7 +411,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 @@ -505,16 +505,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 }) |