Adapt to MC2 and newer versions of Coq · coq-community/lemma-overloading@5e1d123

The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/

"From Coq" has been replaced by "From Stdlib".

"From Coq" has been replaced by "From Stdlib".

Notation nosimpl is deprecated since mathcomp 2.3.0.

Notation nosimpl is deprecated since mathcomp 2.3.0.

"From Coq" has been replaced by "From Stdlib".

Notation nosimpl is deprecated since mathcomp 2.3.0.

Notation nosimpl is deprecated since mathcomp 2.3.0.

Notation nosimpl is deprecated since mathcomp 2.3.0.

Unused variable e might be a misspelled constructor. Use _ or _e to

The default and global localities for this command outside sections

Provide feedback