Skip to content

Merge pull request #564 from math-comp/saturate-export #1513

Merge pull request #564 from math-comp/saturate-export

Merge pull request #564 from math-comp/saturate-export #1513

Triggered via push October 28, 2025 19:02
Status Success
Total duration 4m 37s
Artifacts

main.yml

on: push
Matrix: opam
release
0s
release
Fit to window
Zoom out
Zoom in

Annotations

20 warnings
opam (9.1): HB/structures.v#L35
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
opam (9.1): HB/structures.v#L34
Coq.ssr.ssreflect.Phantom has been replaced by
opam (9.1): HB/structures.v#L33
Coq.ssr.ssreflect.phantom has been replaced by
opam (9.1): HB/structures.v#L32
Coq.ssr.ssreflect.Phant has been replaced by
opam (9.1): HB/structures.v#L31
Coq.ssr.ssreflect.phant has been replaced by
opam (9.1): HB/structures.v#L30
Coq.Init.Specif.sigT has been replaced by Corelib.Init.Specif.sigT.
opam (9.1): HB/structures.v#L29
Coq.Init.Datatypes.prod has been replaced by
opam (9.1): HB/structures.v#L28
Coq.Init.Datatypes.pair has been replaced by
opam (9.1): HB/structures.v#L27
Coq.Init.Datatypes.Some has been replaced by
opam (9.1): HB/structures.v#L24
Coq.Init.Datatypes.None has been replaced by
opam (9.0): HB/structures.v#L35
Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
opam (9.0): HB/structures.v#L34
Coq.ssr.ssreflect.Phantom has been replaced by
opam (9.0): HB/structures.v#L33
Coq.ssr.ssreflect.phantom has been replaced by
opam (9.0): HB/structures.v#L32
Coq.ssr.ssreflect.Phant has been replaced by
opam (9.0): HB/structures.v#L31
Coq.ssr.ssreflect.phant has been replaced by
opam (9.0): HB/structures.v#L30
Coq.Init.Specif.sigT has been replaced by Corelib.Init.Specif.sigT.
opam (9.0): HB/structures.v#L29
Coq.Init.Datatypes.prod has been replaced by
opam (9.0): HB/structures.v#L28
Coq.Init.Datatypes.pair has been replaced by
opam (9.0): HB/structures.v#L27
Coq.Init.Datatypes.Some has been replaced by
opam (9.0): HB/structures.v#L24
Coq.Init.Datatypes.None has been replaced by