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 8282f1402d16791728b9441011d8c5fc6507d266..4309994de9ecd989eecc85999db677cf9880d42d 100644 (file)
--- 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