Skip to content
Docker CI

add MonadTypedStore #360

Sign in to view logs

add MonadTypedStore

add MonadTypedStore #360

Triggered via pull request June 30, 2023 09:45
@garriguegarrigue
synchronize #105
typed_store_monad
Status Success
Total duration 23m 9s
Artifacts –

docker-action.yml

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

Annotations

16 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#L70
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#L76
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#L77
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#L79
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#L95
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#L480
Unused variable ml_undef might be a misspelled constructor. Use _ or
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#L70
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#L76
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#L77
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#L79
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#L95
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#L480
Unused variable ml_undef might be a misspelled constructor. Use _ or