Coq Call 2023 02 08
- February 8th 2023, 4pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
- 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 ofrefine, so thatrefineshelves all evars dependent in the type (as in pre-8.5); this allows to haverapplycloser fromapply#17212 - add support for using either
refineorres_pfinTactics.generic_applyleading to a new family [simple] [e]rapply[in] subsubming Program'srapplyand the various user copies ofrapply(see corresponding branch and discussion on the semantics ofrapplyin #17209)
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.