aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarsolve.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarsolve.ml')
-rw-r--r--pretyping/evarsolve.ml2
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))