X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicSubstitution.ml;h=67eb10a651553956f3798ef5800377115905434b;hb=206dd7a0508b73fd3c18747f4997dddc0a12fc3a;hp=2be7f5871704457a10683e7fd673e76e834b3fc5;hpb=5ba3b166fff4398b031774b52bd7c1ae1e5be09b;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 2be7f5871..67eb10a65 100644
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -49,7 +49,7 @@ let rec psubst ?(avoid_beta_redexes=false) delift lift_args map_arg args =
          if delift && nargs <> 0 then NCic.Rel (n - nargs) else t
       | n when n < k -> t
       | n (* k <= n < k+nargs *) ->
-       (try lift (k+lift_args) (map_arg (List.nth args (n-k)))
+       (try lift (k-1+lift_args) (map_arg (List.nth args (n-k)))
         with Failure _ -> assert false))
    | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
        if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,l)) else t