Overview
Request 824553 accepted
- Update to version 8.12.0.
* New binder notation for non-maximal implicit arguments using []
allowing to set and see the implicit status of arguments
immediately.
* New notation Inductive "I A | x : s := ..." to distinguish the
uniform from the non-uniform parameters in inductive
definitions.
* More robust and expressive treatment of implicit inductive
parameters in inductive declarations.
* Improvements in the treatment of implicit arguments and
partially applied constants in notations, parsing of
hexadecimal number notation and better handling of scopes and
coercions for printing.
* A correct and efficient coercion coherence checking algorithm,
avoiding spurious or duplicate warnings.
* An improved Search command which accepts complex queries. This
takes precedence over the now deprecated ssreflect search.
* Many additions and improvements of the standard library.
* Improvements to the reference manual include a more logical
organization of chapters along with updated syntax descriptions
that match Coq's grammar in most but not all chapters.
- Created by aaronpuchert
- In state accepted
Request History
aaronpuchert created request
- Update to version 8.12.0.
* New binder notation for non-maximal implicit arguments using []
allowing to set and see the implicit status of arguments
immediately.
* New notation Inductive "I A | x : s := ..." to distinguish the
uniform from the non-uniform parameters in inductive
definitions.
* More robust and expressive treatment of implicit inductive
parameters in inductive declarations.
* Improvements in the treatment of implicit arguments and
partially applied constants in notations, parsing of
hexadecimal number notation and better handling of scopes and
coercions for printing.
* A correct and efficient coercion coherence checking algorithm,
avoiding spurious or duplicate warnings.
* An improved Search command which accepts complex queries. This
takes precedence over the now deprecated ssreflect search.
* Many additions and improvements of the standard library.
* Improvements to the reference manual include a more logical
organization of chapters along with updated syntax descriptions
that match Coq's grammar in most but not all chapters.
factory-auto added opensuse-review-team as a reviewer
Please review sources
factory-auto accepted review
Check script succeeded
licensedigger accepted review
ok
dimstar_suse added openSUSE:Factory:Staging:adi:26 as a reviewer
Being evaluated by staging project "openSUSE:Factory:Staging:adi:26"
dimstar_suse accepted review
Picked "openSUSE:Factory:Staging:adi:26"
dimstar accepted review
dimstar_suse accepted review
Staging Project openSUSE:Factory:Staging:adi:26 got accepted.
dimstar_suse approved review
Staging Project openSUSE:Factory:Staging:adi:26 got accepted.
dimstar_suse accepted request
Staging Project openSUSE:Factory:Staging:adi:26 got accepted.