5 files changed, 21 insertions, 3 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f65b5cc3e..c2ded73ad 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -861,15 +861,17 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
 	      aux evd pbs progress (pb :: stuck)
             end
         | UnifFailure (evd,reason) ->
-	    Pretype_errors.error_cannot_unify env evd ~reason (t1, t2))
+	    Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb)
+              env evd ~reason (t1, t2))
     | _ -> 
 	if progress then aux evd stuck false []
 	else 
 	  match stuck with
 	  | [] -> (* We're finished *) evd
-	  | (pbty,env,t1,t2) :: _ ->
+	  | (pbty,env,t1,t2 as pb) :: _ ->
 	      (* There remains stuck problems *)
-	      Pretype_errors.error_cannot_unify env evd (t1, t2)
+	      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
   let heuristic_solved_evd = aux evd pbs false [] in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4208a3763..f9ca6a241 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -477,6 +477,14 @@ let extract_changed_conv_pbs evd p =
 let extract_all_conv_pbs evd =
   extract_conv_pbs evd (fun _ -> true)
 
+let loc_of_conv_pb evd (pbty,env,t1,t2) =
+  match kind_of_term (fst (decompose_app t1)) with
+  | Evar (evk1,_) -> fst (evar_source evk1 evd)
+  | _ ->
+  match kind_of_term (fst (decompose_app t2)) with
+  | Evar (evk2,_) -> fst (evar_source evk2 evd)
+  | _ -> Loc.ghost
+
 (* spiwack: should it be replaced by Evd.merge? *)
 let evar_merge evd evars =
   { evd with evars = EvarMap.merge evd.evars evars.evars }
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 53956f99b..b3866e320 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -201,6 +201,7 @@ val extract_changed_conv_pbs : evar_map ->
       (ExistentialSet.t -> evar_constraint -> bool) ->
       evar_map * evar_constraint list
 val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
+val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t
 
 val evar_list : evar_map -> constr -> existential list
 val collect_evars : constr -> ExistentialSet.t
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f3235b9d1..ec808de0f 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -149,6 +149,10 @@ let error_unsolvable_implicit loc env sigma evi e explain =
   Loc.raise loc
     (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
 
+let error_cannot_unify_loc loc env sigma ?reason (m,n) =
+  let env, m, n = contract2 env m n in
+  Loc.raise loc (PretypeError (env, sigma,CannotUnify (m,n,reason)))
+
 let error_cannot_unify env sigma ?reason (m,n) =
   raise (PretypeError (env, sigma,CannotUnify (m,n,reason)))
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index b57111bc6..36ae6c13f 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -96,6 +96,9 @@ val error_unsolvable_implicit :
   Loc.t -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t ->
       Evd.unsolvability_explanation option -> 'b
 
+val error_cannot_unify_loc : Loc.t -> env -> Evd.evar_map ->
+  ?reason:unification_error -> constr * constr -> 'b
+
 val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error ->
   constr * constr -> 'b