Merge pull request #62 from Tragicus/pr1256 · math-comp/real-closed@21062a5

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/

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.

Notation nosimpl is deprecated since mathcomp 2.3.0.

mid_in is declared opaque (Qed) but this is not fully respected

dern_gt0 is declared opaque (Qed) but this is not fully respected

Notation archiFieldType is deprecated since mathcomp 2.3.0.

Notation archiFieldType is deprecated since mathcomp 2.3.0.

Notation archiFieldType is deprecated since mathcomp 2.3.0.

Notation archiFieldType is deprecated since mathcomp 2.3.0.

Provide feedback