Skip to content

intro upd

intro upd #197

Triggered via push May 30, 2025 14:58
Status Success
Total duration 13m 26s
Artifacts

build.yml

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

Annotations

10 warnings
build (coqorg/coq:8.20): theories/examples/heap_lang/lang.v#L347
Ignoring canonical projection to equivL by ofe_equiv in valO:
build (coqorg/coq:8.20): theories/examples/heap_lang/lang.v#L347
Ignoring canonical projection to discrete_dist by ofe_dist in valO:
build (coqorg/coq:8.20): theories/examples/heap_lang/lang.v#L347
Ignoring canonical projection to discrete_ofe_mixin by ofe_mixin in
build (coqorg/coq:8.20): theories/examples/heap_lang/lang.v#L346
Ignoring canonical projection to equivL by ofe_equiv in locO:
build (coqorg/coq:8.20): theories/examples/heap_lang/lang.v#L346
Ignoring canonical projection to discrete_dist by ofe_dist in locO:
build (coqorg/coq:8.20): theories/examples/heap_lang/lang.v#L346
Ignoring canonical projection to discrete_ofe_mixin by ofe_mixin in
build (coqorg/coq:8.20): theories/examples/heap_lang/lang.v#L345
Ignoring canonical projection to equivL by ofe_equiv in stateO:
build (coqorg/coq:8.20): theories/examples/heap_lang/lang.v#L345
Ignoring canonical projection to discrete_dist by ofe_dist in
build (coqorg/coq:8.20): theories/examples/heap_lang/lang.v#L345
Ignoring canonical projection to discrete_ofe_mixin by ofe_mixin in
build (coqorg/coq:8.20): vendor/Binding/Core.v#L3
Using Vector.t is known to be technically difficult, see