From e77f178e60918f14eacd1ec0364a491d4cfd0f3f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 3 Mar 2015 00:48:34 +0100
Subject: Fix bug introduced by my last commit, forgetting to adjust de Bruijn
 index lookup.

---
 pretyping/evarsolve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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 [])
-- 
cgit v1.2.3