X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=5a85a1289297301031355cf3bf3dfa4cae83f921;hb=39b205d12af34c0c8d6e691da2628bc386b70cf2;hp=ec4747781a646371d729e12098ad523f096d1c8e;hpb=1c4968498b6f108cd9c4074c177845a4067cd9d6;p=helm.git

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), _ =