Skip to content
Docker CI

add MonadTypedStore #354

Sign in to view logs

add MonadTypedStore

add MonadTypedStore #354

Triggered via pull request June 27, 2023 04:15
@garriguegarrigue
synchronize #105
typed_store_monad
Status Success
Total duration 35m 23s
Artifacts –

docker-action.yml

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

Annotations

12 warnings
build (mathcomp/mathcomp:1.16.0-coq-8.17): proba_lib.v#L227
Trying to mask the absolute name "T"!
build (mathcomp/mathcomp:1.16.0-coq-8.17): smallstep.v#L39
The default and global localities for this command outside sections
build (mathcomp/mathcomp:1.16.0-coq-8.17): example_typed_store.v#L68
Use of “Require” inside a module is fragile. It is not recommended
build (mathcomp/mathcomp:1.16.0-coq-8.17): example_typed_store.v#L71
Use of “Require” inside a module is fragile. It is not recommended
build (mathcomp/mathcomp:1.16.0-coq-8.17): example_typed_store.v#L72
Use of “Require” inside a module is fragile. It is not recommended
build (mathcomp/mathcomp:1.16.0-coq-8.17): example_typed_store.v#L73
Use of “Require” inside a module is fragile. It is not recommended
build (mathcomp/mathcomp:1.17.0-coq-8.17): proba_lib.v#L227
Trying to mask the absolute name "T"!
build (mathcomp/mathcomp:1.17.0-coq-8.17): smallstep.v#L39
The default and global localities for this command outside sections
build (mathcomp/mathcomp:1.17.0-coq-8.17): example_typed_store.v#L68
Use of “Require” inside a module is fragile. It is not recommended
build (mathcomp/mathcomp:1.17.0-coq-8.17): example_typed_store.v#L71
Use of “Require” inside a module is fragile. It is not recommended
build (mathcomp/mathcomp:1.17.0-coq-8.17): example_typed_store.v#L72
Use of “Require” inside a module is fragile. It is not recommended
build (mathcomp/mathcomp:1.17.0-coq-8.17): example_typed_store.v#L73
Use of “Require” inside a module is fragile. It is not recommended