From: Enrico Tassi Date: Fri, 4 Apr 2008 17:41:33 +0000 (+0000) Subject: today it seems that the substituted should be lifted by k-1+lift_args and not k+lift_... X-Git-Tag: make_still_working~5445 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dff76b5e1557ff32872f4e48854daaa6c42e5ad2;p=helm.git today it seems that the substituted should be lifted by k-1+lift_args and not k+lift_args since k starts from 1 --- 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