From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 May 2008 17:32:34 +0000 (+0000)
Subject: One more bug fixed: we tried to perform List.nth on negative indexes.
X-Git-Tag: make_still_working~5219
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df28d2c8f26ad18cc8b61b73adb1dfd8be31ec35;p=helm.git

One more bug fixed: we tried to perform List.nth on negative indexes.
---

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