Stop using auto with * in intuition #610
SkySkimmer
This run and associated checks have been archived and are scheduled for deletion.
Learn more about checks retention
Annotations
4 errors and 26 warnings
|
build (coqorg/coq:8.14):
Lib/FMapExt.v#L6
There is no Ltac named Tauto.intuition_solver.
|
|
build (coqorg/coq:8.14):
Lib/Tactics.v#L98
There is no Ltac named Tauto.intuition_solver.
|
|
build (coqorg/coq:8.15):
Lib/MapDecide.v#L61
No such Hint database: map.
|
|
build (coqorg/coq:8.16):
Lib/MapDecide.v#L61
No such Hint database: map.
|
|
build (coqorg/coq:8.14):
Lib/Setoid.v#L4
Notation "_ ++> _" was already used in scope signature_scope.
|
|
build (coqorg/coq:8.14):
Lib/Setoid.v#L4
Notation "_ ==> _" was already used in scope signature_scope.
|
|
build (coqorg/coq:8.14):
Lib/Setoid.v#L4
Notation "_ --> _" was already used in scope signature_scope.
|
|
build (coqorg/coq:8.15):
Lib/Setoid.v#L4
Notation "_ ++> _" was already used in scope signature_scope.
|
|
build (coqorg/coq:8.15):
Lib/Setoid.v#L4
Notation "_ ==> _" was already used in scope signature_scope.
|
|
build (coqorg/coq:8.15):
Lib/Setoid.v#L4
Notation "_ --> _" was already used in scope signature_scope.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L6
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L6
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L8
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L8
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L8
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L8
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L10
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L10
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L10
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:dev):
Instance/Lambda/Ltac.v#L10
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L6
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L6
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L8
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L8
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L8
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L8
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L10
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L10
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L10
Notation "_ ~= _" is deprecated since 8.17.
|
|
build (coqorg/coq:8.17):
Instance/Lambda/Ltac.v#L10
Notation "_ ~= _" is deprecated since 8.17.
|