diff options
| author | Hugo Herbelin | 2020-11-15 13:28:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-15 17:35:03 +0100 |
| commit | 6ae29940af487e03ef2eafc9cb5c9b0d015c6a7c (patch) | |
| tree | 55519570f3570344380cdb970feba7446a0481d6 /pretyping/evarsolve.ml | |
| parent | 4b4ae1345858070a96b70d7d6c043d0ff9f5a4a7 (diff) | |
Fixes #12348: long-standing de Bruijn indices bug in imitation (solve_simple_eqn).
The bug was that an assumption could be interpreted as a local
definition and wrongly expanded.
It triggered rarely because it involved mixing let-ins and
local assumptions + imitation under binders.
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index de41c8f22f..c58ebe1bbd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1576,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)) |