diff options
| author | Hugo Herbelin | 2020-08-21 21:00:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 11:45:32 +0100 |
| commit | a8b25255a5e918ed0d8dfcc8529dcd2ec27f721b (patch) | |
| tree | c4a806c928285159a78ebaebe6b4ae68b8965260 /pretyping | |
| parent | 47c05b2531cb0de6da91968e2d17c68033ae7835 (diff) | |
Checking type in unification imitation: avoid raising a non-located error.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 994ba9e0e7..5548f3205b 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -227,8 +227,7 @@ let recheck_applications unify flags env evdref t = (match unify flags TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with | Success evd -> evdref := evd; aux (succ i) (subst1 args.(i) codom) - | UnifFailure (evd, reason) -> - Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) + | UnifFailure (evd, reason) -> raise (IllTypedInstance (env, ty, argsty.(i)))) | _ -> raise (IllTypedInstance (env, ty, argsty.(i))) else () in aux 0 fty |