]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed off-by-one
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 1 Oct 2009 08:46:21 +0000 (08:46 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 1 Oct 2009 08:46:21 +0000 (08:46 +0000)
helm/software/components/ng_kernel/nCicUntrusted.ml

index fd3fd5f794101b84ad230c8d347e056bfa44fed1..1e7432724bc7b5837a0b9e1f0c65ad121ec5f918 100644 (file)
@@ -178,7 +178,7 @@ let rec fire_projection_redex () = function
         let l' = HExtlib.sharing_map (fire_projection_redex ()) l in
         if l == l' then t else C.Appl l'
       in
-      if (*pragma <> `Projection ||*) List.length args < rno then conclude ()
+      if (*pragma <> `Projection ||*) List.length args <= rno then conclude ()
       else
         (match List.nth args rno with
         | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->