off by one fixed

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index ec4747781a646371d729e12098ad523f096d1c8e..5a85a1289297301031355cf3bf3dfa4cae83f921 100644 (file)
--- 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), _ =