X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicSubstitution.ml;h=43a2f8174a74a1cad4696523908e8a4575f6933e;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=93268e258049898d1156f85637a3e02f2ae65ecf;hpb=30111ae182e35dc2f7aac9ea23746ba671d2001b;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index 93268e258..43a2f8174 100644
--- a/helm/software/components/ng_kernel/nCicSubstitution.ml
+++ b/helm/software/components/ng_kernel/nCicSubstitution.ml
@@ -25,6 +25,7 @@ let debug_print = fun _ -> ();;
 let lift_from k n =
  let rec liftaux k = function
     | C.Rel m as t -> if m < k then t else C.Rel (m + n)
+    | C.Meta (i,(m,(C.Irl 0 as l))) when k <= m+1 -> C.Meta (i,(m,l))
     | C.Meta (i,(m,l)) when k <= m+1 -> C.Meta (i,(m+n,l))
     | C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
     | C.Meta (i,(m,l)) -> 
@@ -62,8 +63,7 @@ let rec psubst ?(avoid_beta_redexes=false) map_arg args =
         with Failure _ | Invalid_argument _ -> assert false))
    | C.Meta (i,(m,l)) as t when m >= k + nargs - 1 -> 
        if nargs <> 0 then C.Meta (i,(m-nargs,l)) else t
-   | C.Meta (i,(m,(C.Irl l as irl))) as t when k > l + m -> 
-       if nargs <> 0 then C.Meta (i,(m-nargs,irl)) else t
+   | C.Meta (_,(m,(C.Irl l))) as t when k > l + m -> t
    | C.Meta (i,(m,l)) -> 
       let lctx = NCicUtils.expand_local_context l in
        C.Meta (i,(0,