From dff76b5e1557ff32872f4e48854daaa6c42e5ad2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Apr 2008 17:41:33 +0000 Subject: [PATCH] today it seems that the substituted should be lifted by k-1+lift_args and not k+lift_args since k starts from 1 --- helm/software/components/ng_kernel/nCicSubstitution.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2