aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 31fb1174a..cd7ce89e0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1253,7 +1253,7 @@ let consider_remaining_unif_problems env
aux evd pbs progress (pb :: stuck)
end
| UnifFailure (evd,reason) ->
- Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb)
+ Pretype_errors.error_cannot_unify ~loc:(loc_of_conv_pb evd pb)
env evd ~reason (t1, t2))
| _ ->
if progress then aux evd stuck false []
@@ -1262,7 +1262,7 @@ let consider_remaining_unif_problems env
| [] -> (* We're finished *) evd
| (pbty,env,t1,t2 as pb) :: _ ->
(* There remains stuck problems *)
- Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb)
+ Pretype_errors.error_cannot_unify ~loc:(loc_of_conv_pb evd pb)
env evd (t1, t2)
in
let (evd,pbs) = extract_all_conv_pbs evd in