diff options
| author | Hugo Herbelin | 2020-11-15 13:27:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-15 17:35:02 +0100 |
| commit | 4b4ae1345858070a96b70d7d6c043d0ff9f5a4a7 (patch) | |
| tree | f3f47eced457b39a9cd599a566d8717ae11f21f9 | |
| parent | 93ee64000d4e121718b4735468626b481b2533bc (diff) | |
Locating the Ill-typed evar instance error.
Even though it is not strongly supposed to be raised.
| -rw-r--r-- | pretyping/evarsolve.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |