Minutes September 23 2020 - math-comp/math-comp GitHub Wiki
licensing: there is no such as as CeCILL-B v2, so Enrico needs to talk with the "Coq wannabe legal team" (no pun intended) a bit more
about PR 501:
not present in easycript, no advise there
ET: I'm ok with this PR, but we must say that it kills support for Coq < 8.10
CC: if the goal is "forall x, G x" /[dup] works and does "forall y x, G x" so that you can play freely with y
About Coq 8.12 search:
little regression in headconcl: since it does not use coercions to make the given expressions into a type (to be reported)
about using predicators PR 548
CC: we need to fix Search w.r.t. unfolding
KS: we also need to declare scope information for predicators, otherwise type inference misbehaves (see the failure in CI on odd-order, https://github.com/math-comp/odd-order/blob/master/theories/PFsection2.v#L168 , x is not in group_scope, but it should since conjg1 is about groups, but the predicator does not set it, while the old code was in some way).
CC: some statements don't fit a predicator without flipping arguments, and this is signalling a bad ordering.
Idea: Coq could understand an attribute term #[also(equivalent term)] so that one could write
left_id 0 (+) #[aka(forall x, 0 + x = x)] and Coq could check that the two are equivalent
CD: it Coq silently ignores the attribute today, then we can support old versions of Coq easily (works also for Search)
About naming in matrix:
we may keep "matrix" in matrixP and row_matrixP and \matrix_ and put mx everywhere else.