- | C.Meta (i,(m,l)) as t when k <= m ->
- if n = 0 then t else C.Meta (i,(m+n,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)) ->
let lctx = NCicUtils.expand_local_context l in
| 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
(* subst t1 t2 *)
(* substitutes [t1] for [Rel 1] in [t2] *)
(* if avoid_beta_redexes is true (default: false) no new beta redexes *)
(* subst t1 t2 *)
(* substitutes [t1] for [Rel 1] in [t2] *)
(* if avoid_beta_redexes is true (default: false) no new beta redexes *)
| 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 *)
(* returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *)
(* [t_i] is lifted as usual when it crosses an abstraction *)
(* returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *)
(* [t_i] is lifted as usual when it crosses an abstraction *)