one main property of lift closed

[helm.git] / matita / components / ng_refiner / nCicMetaSubst.ml

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index 73cc91892788b5b2c033f6fc39b17562f0530bbe..f1fa293b338e866d2042dcbbb4ee6f0ae5b32bc9 100644 (file)
--- 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 ->