-
Notifications
You must be signed in to change notification settings - Fork 111
Agenda of November 14th 2019 meeting 10:00 to 11:00
Enrico Tassi edited this page Nov 14, 2019
·
6 revisions
- next mathcomp release?
- installation instructions (reported from previous meetings)
- followup of the last meeting
- finmap status
- PR 270 status
- documentation for naming conventions of structures and modules (incoming PR on
CONTRIBUTING.md
)
- Coq 8.10 is out, should we release?
- Enrico: takes 3h top, maybe good time since we are in a stable situation
- GG: a finmap related change should go in before, something about general induction, eg
elim: x {2}x (ltnSn x)
; it could break on sets built on finmap since there are more occurrences of the set. We could avoid breakage with an helper lemma. GG does the PR. - Plan: we add the lemma for general induction then we release, RM are GG and Yves
- RM postpone PR and issues from milestone 1.10 to 1.11
- last meeting we thought about a generalization/factoring involving generic quotients. Still to be integrated.
- GG: there is an open design question for predicates on a finite domain
- progress report: 1 renaming to do before merge
- some improvements can be made afterwards
- let's merge just after the release
- merged