The following actions uses Node.js version which is deprecated 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 sub is deprecated since mathcomp 2.0.0. Use Sub instead.

Notation sub is deprecated since mathcomp 2.0.0. Use Sub instead.

Cast types are ignored in patterns

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

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

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

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

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

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