Bug fixed in does_not_occur when a LetIn was found in the context.

diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml
index d2ad6a55f799015fc044550953dd18bf1d649887..343be2607277b7bbab8e4bd0523fc35d9d7d0069 100644 (file)
--- a/matita/components/ng_kernel/nCicTypeChecker.ml
+++ b/matita/components/ng_kernel/nCicTypeChecker.ml
@@ -186,7 +186,7 @@ let does_not_occur status ~subst context n nn t =
     | C.Rel m when m <= k || m > nn+k -> ()
     | C.Rel m ->
         (try match List.nth context (m-1-k) with
-          | _,C.Def (bo,_) -> aux (n-m) () bo
+          | _,C.Def (bo,_) -> aux 0 () (S.lift status (m-k) bo)
           | _ -> ()
          with Failure _ -> assert false)
     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()