- (* 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.Implicit _ -> assert false (* was identity *)
+ C.Meta (i,(0,
+ C.Ctx (HExtlib.sharing_map
+ (fun x -> substaux k (lift ~no_implicit m x)) lctx)))
+ | C.Implicit _ as t ->
+ if no_implicit then assert false (* was identity *)
+ else t