Skip to content

Merge pull request #121 from proux01/fix-macos #87

Merge pull request #121 from proux01/fix-macos

Merge pull request #121 from proux01/fix-macos #87

Triggered via push February 24, 2025 13:55
Status Failure
Total duration 4m 56s
Artifacts
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

34 warnings
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L150
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L153
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L171
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L173
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L186
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L188
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L190
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L236
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L358
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp-dev:coq-8.20): finmap.v#L360
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L150
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L153
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L171
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L173
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L186
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L188
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L190
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L236
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L358
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp-dev:rocq-prover-dev): finmap.v#L360
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.1.0-coq-8.18): finmap.v#L612
HB: no new instance is generated
build (mathcomp/mathcomp:2.1.0-coq-8.18): finmap.v#L613
HB: no new instance is generated
build (mathcomp/mathcomp:2.2.0-coq-8.19): finmap.v#L612
HB: no new instance is generated
build (mathcomp/mathcomp:2.2.0-coq-8.19): finmap.v#L613
HB: no new instance is generated
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L150
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L153
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L171
Notations "[ fset _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L173
Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L186
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L188
Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L190
Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L236
Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L358
Postfix notations (i.e. starting with a nonterminal symbol and
build (mathcomp/mathcomp:2.3.0-coq-8.20): finmap.v#L360
Postfix notations (i.e. starting with a nonterminal symbol and