From 4b54dde3aab6d58ab11c5bafd291b65af241e28e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 Jun 2011 21:05:44 +0000 Subject: [PATCH] Possible assert false case implemented --- matita/components/ng_refiner/nCicMetaSubst.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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 -> -- 2.39.2