X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicSubstitution.ml;h=43a2f8174a74a1cad4696523908e8a4575f6933e;hb=134d8273511016e9b6de3423d301a080046f3948;hp=c9413fcab89e3910d09b84e4ae923b29c5571d03;hpb=22574214f7ab6b0ce7de37b50cad2037074c51b0;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml
index c9413fcab..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,7 +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 -> 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,