From 4b4ae1345858070a96b70d7d6c043d0ff9f5a4a7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Nov 2020 13:27:43 +0100
Subject: Locating the Ill-typed evar instance error.

Even though it is not strongly supposed to be raised.
---
 pretyping/evarsolve.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 715b80f428..de41c8f22f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -810,7 +810,8 @@ let check_evar_instance unify flags env evd evk1 body =
   (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
   let ty =
     try Retyping.get_type_of ~lax:true evenv evd body
-    with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance"))
+    with Retyping.RetypeError _ ->
+      let loc, _ = evi.evar_source in user_err ?loc (Pp.(str "Ill-typed evar instance"))
   in
   match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with
   | Success evd -> evd
-- 
cgit v1.2.3