• Björn Brandenburg's avatar
    port existing proofs to ssreflect 1.9.0 · 09703078
    Björn Brandenburg authored
    From the mathcomp 1.9.0 release notes:
    > removed Coq prelude hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm, to
    > improve robustness of by ...; scripts may need to invoke addn0,
    > addnS, muln0 or mulnS explicitly where these hints were used
    > accidentally.
    => This patch makes these required fixes in Prosa.
    While at it, turn on CI for coq:dev and Coq 8.9 with two versions of ssreflect.
suspension_intervals.v 22.5 KB