From 8c8ee30d3de315e954a59b3e802748099a32b54c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 15 May 2012 20:47:27 +0000 Subject: [PATCH] Bug fixed in does_not_occur when a LetIn was found in the context. --- matita/components/ng_kernel/nCicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml index d2ad6a55f..343be2607 100644 --- 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 *) () -- 2.39.2