Support mathcomp 1.11.0 and Coq 8.12

There were a number of breaking changes and a ton of deprecation warnings that this MR fixes. Supporting both mathcomp 1.10.0 and 1.11.0 turned out to require some contortions.

Note: this drops support for mathcomp < 1.10.0 and Coq < 8.11.

CC: @proux @sophie @mlesourd @ptorrx

merged

Sorry for the late answer and thanks for taking care of this!

A few minor comments:

• in coq-prosa.opam shouldn't >= 8.10 be >= 8.11? (I'm opening a separate merge request)
• maybe is this worth a new release so that there is a stable release of Prosa available for the last version of Coq (I can take care of the OPAM stuff)
• the replacement of by with now is probably reasonable here, however I tend to think that by should be preferred to now (which is a notation for ; easy as defined in https://github.com/coq/coq/blob/master/theories/Init/Tactics.v#L166) not just because it is the ssreflect version of it but also because, being more powerful, the latter can sometime be slower
• FYI, ssrlia should be provided with mathcomp in the future and we should ultimately be able to get rid of it https://github.com/math-comp/math-comp/issues/263#issuecomment-631377939

mentioned in merge request !105 (merged)

Thanks for the pointers! Looking forward to phasing out ssrlia in the future. Though we probably won't require 8.13 until some time next year at the earliest, so the changes are still required and useful now.

A new release would indeed make sense. I don't see any major developments pending that should be merged first (also there's always the next release), so I think we could just tag the current version and go ahead.

On now vs by, I wasn't aware that there's a technical difference (in fact, I wasn't aware of now at all until Sergey pointed it out). The reason why we've started preferring now over by is because emacs wrongly indents by…

The indentation comes from historical reasons with its use in casual (non ssreflect) scripts.

It seems that the Emacs indentation can be fixed by adding '(coq-smie-user-tokens (quote (("by" . "now")))) in custom-set-variables in your .emacs to have by indented as now.