• warnings we are ignoring & duplicate CS declarations

• integration of fcsl-pcm? (#435)

Minutes

• PR #435 has been merged. Furthermore, some how-do should be extracted from this PR and added to the documentation that explains how to add a project to the math-comp CI.

• Warning about CS could be removed thanks to new Coq features. Enrico will evaluate the feasability for the next meeting. Anton asks if something could be done about the Notation warning that are triggered when doing an import. Enrico replies that we should ask Maxime if this is feasable. Also, Yves raises the issue that the flags to silent warnings are duplicated between _CoqProject and Makefile. A discussion about theses warnings and the flags should be discussed in a next meeting.

• 8.11 is about to be released. Laurent asks if we should also do a new release. Enrico says that the current release of mathcomp is ok with 8.11. Reynald said that we are not ready for a new release as some developments (like comp-analysis) are not in sync with master. The need for a new release will be discussed in the next meeting

• As in 2-week time there is Popl, the next meeting will be on January, 30th.