Coq Call 2021 03 24
- March 24th 2021, 4pm-5pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
- PRS about typeclasses, and what where should we go from there. (Matthieu)
asserting scopes on syndef arguments https://github.com/coq/coq/pull/13965 (Enrico)
- PRS about typeclasses.
- Look into using the same uniform error messaging code
- Long discussion about the design of Hint Extern If tac Then ... and possibly more
expressive variants:
We came to settle on keeping the
Hint Extern Ifwhich allows to express one "global" cut on brothers in the proof search tree + a reference to "self"/continue for solving subgoals with the right options/depth/db etc. One can then useoncefor internal cuts if needed.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq 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.