X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=f1fa293b338e866d2042dcbbb4ee6f0ae5b32bc9;hb=7199d719bd64001e3f71326bea72b3e3f88b7ace;hp=73cc91892788b5b2c033f6fc39b17562f0530bbe;hpb=7aeec317f639936095e10f88cc0b2710262082d0;p=helm.git

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 73cc91892..f1fa293b3 100644
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -57,8 +57,7 @@ exception NotFound of [`NotInTheList | `NotWellTyped];;
 
 let position to_skip n (shift, lc) =
   match lc with
-  | NCic.Irl _ when to_skip > 0 -> assert false  (* unclear to me *)
-  | NCic.Irl len when n <= shift || n > shift + len ->
+  | NCic.Irl len when n <= shift + to_skip || n > shift + len ->
      raise (NotFound `NotInTheList)
   | NCic.Irl _ -> n - shift
   | NCic.Ctx tl ->