From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 17 Jun 2010 21:41:00 +0000 (+0000)
Subject: off by one fixed
X-Git-Tag: make_still_working~2895
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=62ab884c6ce7dd41c6e6fa2efc5102b23f57de32;p=helm.git

off by one fixed
---

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index ec4747781..5a85a1289 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -1135,7 +1135,7 @@ let typeof_obj
                   | NCic.Meta _ -> metasenv, subst
                   | NCic.Implicit _ -> metasenv, subst
                   | NCic.Appl (NCic.Rel i :: args) as t
-                      when i >= List.length context - len ->
+                      when i > List.length context - len ->
                       let lefts, _ = HExtlib.split_nth leftno args in
                       let ctxlen = List.length context in
                       let (metasenv, subst), _ =