wrapper mixin step0 #1033
ptorrxAnnotations
1 error and 44 warnings
|
plan-B:
tests/monoid_law_structure_clone.v#L17
HB: all mixins must have the same key
|
|
opam (8.15)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
opam (8.15):
structures.v#L282
This command does not support this attribute: arguments.
|
|
opam (8.15):
structures.v#L312
This command does not support this attribute: arguments.
|
|
opam (8.15):
structures.v#L345
This command does not support this attribute: arguments.
|
|
opam (8.15):
structures.v#L386
This command does not support this attribute: arguments.
|
|
opam (8.15):
structures.v#L414
This command does not support this attribute: arguments.
|
|
opam (8.15):
structures.v#L462
This command does not support this attribute: arguments.
|
|
opam (8.15)
constant coq.lookup! has no declared type.
|
|
opam (8.15):
structures.v#L629
This command does not support this attribute: arguments.
|
|
opam (8.15):
structures.v#L683
This command does not support this attribute: arguments.
|
|
opam (8.15):
structures.v#L714
This command does not support this attribute: arguments.
|
|
plan-B
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
plan-B:
structures.v#L30
ID is linear: name it _ID (discard) or ID_ (fresh variable)
|
|
plan-B:
structures.v#L33
KID is linear: name it _KID (discard) or KID_ (fresh variable)
|
|
plan-B:
structures.v#L33
ID is linear: name it _ID (discard) or ID_ (fresh variable)
|
|
plan-B
constant coq.lookup! has no declared type.
|
|
plan-B
constant coq.gref->modname has no declared type.
|
|
plan-B
Key is linear: name it _Key (discard) or Key_ (fresh variable)
|
|
plan-B
N0 is linear: name it _N0 (discard) or N0_ (fresh variable)
|
|
plan-B
Mixin is linear: name it _Mixin (discard) or Mixin_ (fresh variable)
|
|
plan-B
Body is linear: name it _Body (discard) or Body_ (fresh variable)
|
|
plan-B
N0 is linear: name it _N0 (discard) or N0_ (fresh variable)
|
|
opam (8.16)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
opam (8.16):
structures.v#L30
ID is linear: name it _ID (discard) or ID_ (fresh variable)
|
|
opam (8.16):
structures.v#L33
KID is linear: name it _KID (discard) or KID_ (fresh variable)
|
|
opam (8.16):
structures.v#L33
ID is linear: name it _ID (discard) or ID_ (fresh variable)
|
|
opam (8.16)
constant coq.lookup! has no declared type.
|
|
opam (8.16)
constant coq.gref->modname has no declared type.
|
|
opam (8.16)
Key is linear: name it _Key (discard) or Key_ (fresh variable)
|
|
opam (8.16)
N0 is linear: name it _N0 (discard) or N0_ (fresh variable)
|
|
opam (8.16)
Mixin is linear: name it _Mixin (discard) or Mixin_ (fresh variable)
|
|
opam (8.16)
Body is linear: name it _Body (discard) or Body_ (fresh variable)
|
|
opam (8.16)
N0 is linear: name it _N0 (discard) or N0_ (fresh variable)
|
|
opam (8.17)
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/
|
|
opam (8.17):
structures.v#L30
ID is linear: name it _ID (discard) or ID_ (fresh variable)
|
|
opam (8.17):
structures.v#L33
KID is linear: name it _KID (discard) or KID_ (fresh variable)
|
|
opam (8.17):
structures.v#L33
ID is linear: name it _ID (discard) or ID_ (fresh variable)
|
|
opam (8.17)
constant coq.lookup! has no declared type.
|
|
opam (8.17)
constant coq.gref->modname has no declared type.
|
|
opam (8.17)
Key is linear: name it _Key (discard) or Key_ (fresh variable)
|
|
opam (8.17)
N0 is linear: name it _N0 (discard) or N0_ (fresh variable)
|
|
opam (8.17)
Mixin is linear: name it _Mixin (discard) or Mixin_ (fresh variable)
|
|
opam (8.17)
Body is linear: name it _Body (discard) or Body_ (fresh variable)
|
|
opam (8.17)
N0 is linear: name it _N0 (discard) or N0_ (fresh variable)
|