pass arguments to Ltac definitions as open_constr rather than constr #17087 (seems to better fits the needs, see e.g. this comment)
align the insertion of maximal implicit arguments in ltac non-strict mode to the one done in strict mode #17084
check statically ltac:(...) in terms and body of notations #17085
either change refine, or add an appropriate variant of refine, so that refine shelves all evars dependent in the type (as in pre-8.5); this allows to have rapply closer from apply#17212
add support for using either refine or res_pf in Tactics.generic_apply leading to a new family [simple] [e]rapply [in] subsubming Program's rapply and the various user copies of rapply (see corresponding branch and discussion on the semantics of rapply in #17209)