Add support for more assembly #568
JasonGrosscoq-archlinux.yml
on: pull_request
Annotations
5 errors
|
archlinux:
src/Assembly/Symbolic.v#L4051
In environment
ri : N
r := widest_register_of_index ri : REG
The term "inl (N.to_nat ri)" has type "(nat + ?B)%type"
while it is expected to have type "(N + REG)%type" (cannot unify
"nat" and "N").
|
|
archlinux
Makefile.coq:818: src/Assembly/Symbolic.v
|
|
archlinux
Makefile.coq:818: src/Assembly/Symbolic.v
|
|
archlinux
Process completed with exit code 2.
|
|
archlinux-check-all
Process completed with exit code 1.
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
ExtractionHaskell-archlinux
|
6.29 KB |
sha256:7e202ba66d38bfda25a8e8bf0fb6368939858b119d929f745d408ee20e01676c
|
|
|
ExtractionOCaml-archlinux
|
5.86 KB |
sha256:48af7a90c4f90cf512e6a4eb446cefc39c8fb6612591ae26a2356c2b6947887a
|
|
|
generated-files-archlinux
|
4.87 MB |
sha256:2df768b4f470356a389f0e90c16bfe1499b7852bd6ef36f1631d9b249a5f2abd
|
|
|
timing-files-archlinux
|
1.72 MB |
sha256:3957c912f2d300c2f6d1596d0691545a61ae2eb799cf3ce4b49f26a2fae90343
|
|