Overview

Request 1184115 accepted

- Update to version 8.19.2.
* Fixed a regression from Coq 8.18 in the presence of a defined
field in a primitive `Record`.
* Fixed an issue where the printer was sometimes failing to use a
prefix or infix custom notation whose right-hand side refers to
a different custom entry.
* Fixed `abstract` failure in the presence of admitted goals in
the surrounding proof.
* Fixed issues when using Ltac2 in VsCoq due to incorrect state
handling of Ltac2 notations.
* Fixed `Include` on a module containing a record declared with
`Primitive Projections`.
* Fixed an issue in `Fixpoint` with no arguments.
* Position error/warning tooltips correctly when multibyte UTF-8
characters are present.

Loading...
Request History
Aaron Puchert's avatar

aaronpuchert created request

- Update to version 8.19.2.
* Fixed a regression from Coq 8.18 in the presence of a defined
field in a primitive `Record`.
* Fixed an issue where the printer was sometimes failing to use a
prefix or infix custom notation whose right-hand side refers to
a different custom entry.
* Fixed `abstract` failure in the presence of admitted goals in
the surrounding proof.
* Fixed issues when using Ltac2 in VsCoq due to incorrect state
handling of Ltac2 notations.
* Fixed `Include` on a module containing a record declared with
`Primitive Projections`.
* Fixed an issue in `Fixpoint` with no arguments.
* Position error/warning tooltips correctly when multibyte UTF-8
characters are present.


Factory Auto's avatar

factory-auto added opensuse-review-team as a reviewer

Please review sources


Factory Auto's avatar

factory-auto accepted review

Check script succeeded


Saul Goodman's avatar

licensedigger accepted review

ok


Ana Guerrero's avatar

anag+factory added openSUSE:Factory:Staging:adi:36 as a reviewer

Being evaluated by staging project "openSUSE:Factory:Staging:adi:36"


Ana Guerrero's avatar

anag+factory accepted review

Picked "openSUSE:Factory:Staging:adi:36"


Dominique Leuenberger's avatar

dimstar accepted review


Dominique Leuenberger's avatar

dimstar_suse accepted review

Staging Project openSUSE:Factory:Staging:adi:36 got accepted.


Dominique Leuenberger's avatar

dimstar_suse approved review

Staging Project openSUSE:Factory:Staging:adi:36 got accepted.


Dominique Leuenberger's avatar

dimstar_suse accepted request

Staging Project openSUSE:Factory:Staging:adi:36 got accepted.

openSUSE Build Service is sponsored by