diff options
| author | Matthieu Sozeau | 2015-03-03 00:48:34 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-03-03 00:48:34 +0100 |
| commit | e77f178e60918f14eacd1ec0364a491d4cfd0f3f (patch) | |
| tree | 56b6106b1678e927bb31019e1b249106cc8bd801 | |
| parent | 022ec07048962ccd33ffdbcdc06adcb7fb09924f (diff) | |
Fix bug introduced by my last commit, forgetting to adjust de Bruijn
index lookup.
| -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 db7f6f6772..99d83a0e88 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -189,7 +189,7 @@ let noccur_evar env evd evk c = else Array.iter (occur_rec acc) args') | Rel i when i > k -> if not (Int.Set.mem (i-k) !cache) then - (match pi2 (Environ.lookup_rel (i-k) env) with + (match pi2 (Environ.lookup_rel i env) with | None -> () | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c []) |