Skip to content
Docker CI

Adapt to rocq-prover/rocq#21380. #75

Sign in to view logs

Adapt to rocq-prover/rocq#21380.

Adapt to rocq-prover/rocq#21380. #75

Triggered via pull request November 29, 2025 15:15
@ppedrotppedrot
opened #211
ppedrot:rm-deprecated-9.0
Status Success
Total duration 3m 4s
Artifacts –

docker-action.yml

on: pull_request
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

10 warnings
build (rocq/rocq-prover:dev)
Implicitly declaring hint databases is deprecated. Please explicitly
build (rocq/rocq-prover:dev): theories/Tactics/Hints.v#L74
Implicitly declaring Rewrite hint databases is deprecated. Please
build (rocq/rocq-prover:dev): theories/Tactics/Hints.v#L59
Implicitly declaring Rewrite hint databases is deprecated. Please
build (rocq/rocq-prover:dev): theories/Tactics/Hints.v#L47
Implicitly declaring Rewrite hint databases is deprecated. Please
build (rocq/rocq-prover:dev): theories/Tactics/Hints.v#L38
Implicitly declaring Rewrite hint databases is deprecated. Please
build (rocq/rocq-prover:dev): theories/Tactics/Hints.v#L4
Implicitly declaring Rewrite hint databases is deprecated. Please
build (rocq/rocq-prover:dev): theories/Tactics/Reflect.v#L208
Implicitly declaring Rewrite hint databases is deprecated. Please
build (rocq/rocq-prover:dev): theories/Tactics/Reflect.v#L166
Implicitly declaring Rewrite hint databases is deprecated. Please
build (rocq/rocq-prover:dev): theories/Tactics/Reflect.v#L128
Implicitly declaring Rewrite hint databases is deprecated. Please
build (rocq/rocq-prover:dev): theories/Tactics/Reconstr.v#L15
Implicitly declaring Rewrite hint databases is deprecated. Please