Minutes January 30 2020

Minutes:

• About #453 PY says he tested it and it looks OK
• PY added to the core team so that he can take care of #453
• About #429 the title is only partially describing the change, it should be updated as well as the changelog
• GG takes #429 as an assignee
• About the duplicate/ignored CS warnings
  • sometimes you can't name the field _ since next fields use it
  • you can't use unkeyed to silence the warning since it triggers another warning (no key in the canon value)
    • Coq could be fixed to recognize it and not issue a warning
  • the #[attribute] to avoid indexing a field is in Coq 8.11, so we need to wait a bit
  • changing the semantics of Canonical so that the last command issued wins (as the rest of Coq commands) should not break MC in fundamental ways
  • changing the semantics of Coercions is going to require to reverse the order of the declarations (the redundant ones).
    • We could change Coq so that it always prefers the shortest path, no matter which order you declare them.
• Being in the MC organization is mainly about visibility, projects don't need to adhere to coding standards unless they are meant to become part of MC proper. Your CI should test against MC master and older so that you can tell which versions you support. This should go in the WIKI.