| 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 (i,(m,l)) ->
let lctx = NCicUtils.expand_local_context l in
| 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 (i,(m,l)) ->
let lctx = NCicUtils.expand_local_context l in
- (* 1-nargs < k-m, when <= 0 is still reasonable because we will
- * substitute args[ k-m ... k-m+nargs-1 > 0 ] *)
- C.Meta (i,(m, C.Ctx (HExtlib.sharing_map (substaux (k-m)) lctx)))
+ C.Meta (i,(0,
+ C.Ctx (HExtlib.sharing_map (fun x -> substaux k (lift m x)) lctx)))
| C.Implicit _ -> assert false (* was identity *)
| C.Appl (he::tl) as t ->
(* Invariant: no Appl applied to another Appl *)
| C.Implicit _ -> assert false (* was identity *)
| C.Appl (he::tl) as t ->
(* Invariant: no Appl applied to another Appl *)