diff options
| author | coqbot-app[bot] | 2020-11-16 12:09:04 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 12:09:04 +0000 |
| commit | 8a1e9bb57462614028eb1b3905fb1df1cdf3a871 (patch) | |
| tree | e21b0c0097837167f199f6e0209491773f2502ff /pretyping | |
| parent | deb4206e287d46d804be6c50a06c4544d8ec43cf (diff) | |
| parent | 603023b3e65fe362d0287f9fc6e986ec9ef16684 (diff) | |
Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part of unification
Reviewed-by: mattam82
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 715b80f428..c58ebe1bbd 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 @@ -1575,7 +1576,7 @@ let rec invert_definition unify flags choose imitate_defs match EConstr.kind !evdref t with | Rel i when i>k -> let open Context.Rel.Declaration in - (match Environ.lookup_rel (i-k) env' with + (match Environ.lookup_rel i env' with | LocalAssum _ -> project_variable (RelAlias (i-k)) | LocalDef (_,b,_) -> try project_variable (RelAlias (i-k)) |