From df28d2c8f26ad18cc8b61b73adb1dfd8be31ec35 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 May 2008 17:32:34 +0000
Subject: [PATCH] One more bug fixed: we tried to perform List.nth on negative
 indexes.

---
 helm/software/components/ng_kernel/nCicTypeChecker.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 8282f1402..4309994de 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -220,7 +220,7 @@ exception DoesOccur;;
 let does_not_occur ~subst context n nn t = 
   let rec aux k _ = function
     | C.Rel m when m > n+k && m <= nn+k -> raise DoesOccur
-    | C.Rel m when m > nn+k -> ()
+    | 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
-- 
2.39.2