Coq Call 2023 02 08

• February 8th 2023, 4pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• A couple of "smoothing" of Ltac (HH):
  • strict_check flag made functional #16935
  • 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)

Notes