Overview
Request 1038367 accepted
- Update to version 8.16.1.
* Fixed the conversion of `Prod` values in the native compiler.
* Added `SProp` check for opaque names in conversion.
* Pass the correct environment to compute η-expansion of
cofixpoints in VM and native compilation.
* Fixed an inconsistency with conversion of primitive arrays, and
associated incomplete strong normalization of primitive arrays
with `lazy`.
* `Print Assumptions` treats opaque definitions with missing
proofs (as found in .vos files, produced using -vos) as axioms
instead of ignoring them.
- Created by aaronpuchert
- In state accepted
Request History
aaronpuchert created request
- Update to version 8.16.1.
* Fixed the conversion of `Prod` values in the native compiler.
* Added `SProp` check for opaque names in conversion.
* Pass the correct environment to compute η-expansion of
cofixpoints in VM and native compilation.
* Fixed an inconsistency with conversion of primitive arrays, and
associated incomplete strong normalization of primitive arrays
with `lazy`.
* `Print Assumptions` treats opaque definitions with missing
proofs (as found in .vos files, produced using -vos) as axioms
instead of ignoring them.
factory-auto added opensuse-review-team as a reviewer
Please review sources
factory-auto accepted review
Check script succeeded
staging-bot added openSUSE:Factory:Staging:adi:3 as a reviewer
Being evaluated by staging project "openSUSE:Factory:Staging:adi:3"
staging-bot accepted review
Picked "openSUSE:Factory:Staging:adi:3"
licensedigger accepted review
ok
dimstar accepted review
dimstar_suse accepted review
Staging Project openSUSE:Factory:Staging:adi:3 got accepted.
dimstar_suse approved review
Staging Project openSUSE:Factory:Staging:adi:3 got accepted.
dimstar_suse accepted request
Staging Project openSUSE:Factory:Staging:adi:3 got accepted.
