Skip to content
Back to pull request #119

Stop using auto with * in intuition #77

Sign in to view logs

Stop using auto with * in intuition

Stop using auto with * in intuition #77

Triggered via pull request July 5, 2023 12:55
@SkySkimmerSkySkimmer
opened #119
SkySkimmer:intuit-auto
Status Success
Total duration 3m 6s
Artifacts –

docker-action.yml

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

Annotations

10 warnings
build (coqorg/coq:dev): tests/Test.v#L30
Notation "_ :: _" was already used in scope list_scope.
build (coqorg/coq:dev): tests/Test.v#L79
Notation "_ ++ _" was already used in scope list_scope.
build (coqorg/coq:dev): tests/Test.v#L86
Notation "_ :: _" was already used in scope list_scope.
build (coqorg/coq:dev): tests/Test.v#L87
Notation "_ ++ _" was already used in scope list_scope.
build (coqorg/coq:dev): tests/Test.v#L214
Adding and removing hints in the core database implicitly is
build (coqorg/coq:dev): tests/Test.v#L365
Unused variable other might be a misspelled constructor. Use _ or
build (coqorg/coq:dev): tests/Test.v#L373
Unused variable other might be a misspelled constructor. Use _ or
build (coqorg/coq:dev): tests/Test.v#L415
Unused introduction pattern: hl
build (coqorg/coq:dev): tests/Test.v#L569
Notation gt_irrefl is deprecated since 8.16.
build (coqorg/coq:dev): tests/Test.v#L569
Notation gt_irrefl is deprecated since 8.16.