- Update to version 8.19.1.
* Fixed incorrect abstraction of sort variables for opaque constants leading to an inconsistency. * Fixed memory corruption with `vm_compute` (rare but more likely with OCaml 5.1). * "Found no matching notation to enable or disable" is now a warning instead of an error. * Fixed undeclared universe with multiple uses of `abstract`. * Fixed incorrect printing of constructor values with multiple arguments, and over-parenthesizing of constructor printing. * Fixed incorrect declared type for Ltac2.FMap.fold. OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=63
This commit is contained in:
parent
10555467e2
commit
8870b507b6
@ -1,3 +0,0 @@
|
||||
version https://git-lfs.github.com/spec/v1
|
||||
oid sha256:17e5c10fadcd3cda7509d822099a892fcd003485272b56a45abd30390f6a426f
|
||||
size 7674352
|
3
coq-8.19.1.tar.gz
Normal file
3
coq-8.19.1.tar.gz
Normal file
@ -0,0 +1,3 @@
|
||||
version https://git-lfs.github.com/spec/v1
|
||||
oid sha256:1e535ed924234f18394efce94b12d9247a67e8af29241eb79615804160f21674
|
||||
size 7675945
|
@ -1,3 +0,0 @@
|
||||
version https://git-lfs.github.com/spec/v1
|
||||
oid sha256:dfb1cb81e5602aeb0d0ac409d706abf89b35400eb31c868a6927e1a08d19a824
|
||||
size 7608812
|
3
coq-refman-8.19.1.tar.xz
Normal file
3
coq-refman-8.19.1.tar.xz
Normal file
@ -0,0 +1,3 @@
|
||||
version https://git-lfs.github.com/spec/v1
|
||||
oid sha256:ec71ef3d520b51cba8de84308357945d28f3723f21a56bc64af040c109584c00
|
||||
size 7616556
|
@ -1,3 +0,0 @@
|
||||
version https://git-lfs.github.com/spec/v1
|
||||
oid sha256:ed0e368789eda9a1a0ae0ab7a5f3cbb74f7ee836e96e3eb194f778b19457ec14
|
||||
size 2148484
|
3
coq-stdlib-8.19.1.tar.xz
Normal file
3
coq-stdlib-8.19.1.tar.xz
Normal file
@ -0,0 +1,3 @@
|
||||
version https://git-lfs.github.com/spec/v1
|
||||
oid sha256:0f439c599fe9daee89b9bc3f9df8d3ced238deb30ccef4c3ac4c6ecf64a91b11
|
||||
size 2148396
|
15
coq.changes
15
coq.changes
@ -1,3 +1,18 @@
|
||||
-------------------------------------------------------------------
|
||||
Thu Mar 7 22:31:46 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
|
||||
|
||||
- Update to version 8.19.1.
|
||||
* Fixed incorrect abstraction of sort variables for opaque
|
||||
constants leading to an inconsistency.
|
||||
* Fixed memory corruption with `vm_compute` (rare but more
|
||||
likely with OCaml 5.1).
|
||||
* "Found no matching notation to enable or disable" is now a
|
||||
warning instead of an error.
|
||||
* Fixed undeclared universe with multiple uses of `abstract`.
|
||||
* Fixed incorrect printing of constructor values with multiple
|
||||
arguments, and over-parenthesizing of constructor printing.
|
||||
* Fixed incorrect declared type for Ltac2.FMap.fold.
|
||||
|
||||
-------------------------------------------------------------------
|
||||
Sun Jan 28 20:20:35 UTC 2024 - Aaron Puchert <aaronpuchert@alice-dsl.net>
|
||||
|
||||
|
6
coq.spec
6
coq.spec
@ -26,7 +26,7 @@
|
||||
%endif
|
||||
|
||||
Name: coq
|
||||
Version: 8.19.0
|
||||
Version: 8.19.1
|
||||
Release: 0
|
||||
Summary: Proof Assistant based on the Calculus of Inductive Constructions
|
||||
License: LGPL-2.1-only
|
||||
@ -185,10 +185,10 @@ find %{buildroot}%{_libdir} -name '*.a' \
|
||||
# pushd doc
|
||||
# git sparse-checkout add V%{version}
|
||||
# cd V%{version}
|
||||
# tar --sort=name --owner=0 --group=0 --mtime="@$(stat -c %%Y refman/index.html)" \
|
||||
# tar --sort=name --owner=0 --group=0 --mtime="@${SOURCE_DATE_EPOCH}" \
|
||||
# --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
|
||||
# -cJf ../../coq-refman-%{version}.tar.xz refman
|
||||
# tar --sort=name --owner=0 --group=0 --mtime="@$(stat -c %%Y stdlib/index.html)" \
|
||||
# tar --sort=name --owner=0 --group=0 --mtime="@${SOURCE_DATE_EPOCH}" \
|
||||
# --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
|
||||
# -cJf ../../coq-stdlib-%{version}.tar.xz stdlib
|
||||
# popd
|
||||
|
@ -46,6 +46,10 @@
|
||||
<url type="contribute">https://github.com/coq/coq/blob/master/CONTRIBUTING.md</url>
|
||||
<launchable type="desktop-id">fr.inria.coq.coqide.desktop</launchable>
|
||||
<releases>
|
||||
<release version="8.19.1" date="2024-03-04"/>
|
||||
<release version="8.19.0" date="2024-01-24"/>
|
||||
<release version="8.18.0" date="2023-09-08"/>
|
||||
<release version="8.17.1" date="2023-06-27"/>
|
||||
<release version="8.17.0" date="2023-03-27"/>
|
||||
<release version="8.16.1" date="2022-11-25"/>
|
||||
<release version="8.16.0" date="2022-09-05"/>
|
||||
|
Loading…
Reference in New Issue
Block a user