today it seems that the substituted should be lifted by k-1+lift_args and not k+lift_...

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 2be7f5871704457a10683e7fd673e76e834b3fc5..67eb10a651553956f3798ef5800377115905434b 100644 (file)
--- 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