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 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

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

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

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