Rebuild for ocaml-ppx-deriving 6.1.3

Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild
OCaml 5.5.0 rebuild
2026-07-29 12:32:20 -06:00 · 2026-07-17 08:48:20 +00:00 · 2026-07-09 20:52:51 -06:00 · 2026-04-16 12:23:41 -06:00 · 2026-03-19 21:38:47 -06:00 · 2026-02-21 00:12:57 +00:00
6 changed files with 915 additions and 646 deletions
--- a/534
+++ b/534
@ -0,0 +1,534 @@
+* Mon Oct 14 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-10
+- Fix the location of the icon
+
+* Sun Oct  6 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-9
+- Rebuild for ocaml-re 1.13.3
+
+* Mon Aug  5 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-8
+- Rebuild for ocaml-menhir 20240715, ocaml-ppxlib 0.33.0, and ocaml-zip 1.1.2
+
+* Sat Jul 20 2024 Fedora Release Engineering <releng@fedoraproject.org> - 1.7.2-7
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
+
+* Tue Jul 16 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-6
+- Rebuild for ocaml-zarith 1.14
+
+* Wed Jul  3 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-5
+- Rebuild for ocaml-ppx-sexp-conv 0.17.0
+
+* Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 1.7.2-4
+- OCaml 5.2.0 ppc64le fix
+
+* Thu Jun 13 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-3
+- Rebuild for apron 0.9.15
+- New upstream URL
+
+* Thu May 30 2024 Richard W.M. Jones <rjones@redhat.com> - 1.7.2-2
+- OCaml 5.2.0 for Fedora 41
+
+* Thu Apr 18 2024 Jerry James <loganjerry@gmail.com> - 1.7.2-1
+- Version 1.7.2
+
+* Mon Mar 25 2024 Richard W.M. Jones <rjones@redhat.com> - 1.7.1-3
+- Use %%{bash_completions_dir} macro
+
+* Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 1.7.1-2
+- Build again because koji ran out of disk space
+
+* Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 1.7.1-1
+- Version 1.7.1
+
+* Sat Jan 27 2024 Fedora Release Engineering <releng@fedoraproject.org> - 1.7.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
+* Tue Jan  2 2024 Jerry James <loganjerry@gmail.com> - 1.7.0-1
+- Version 1.7.0
+- Drop upstreamed coq patch
+
+* Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 1.6.0-9
+- OCaml 5.1.1 + s390x code gen fix for Fedora 40
+
+* Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 1.6.0-8
+- OCaml 5.1.1 rebuild for Fedora 40
+
+* Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 1.6.0-7
+- OCaml 5.1 rebuild for Fedora 40
+
+* Sat Sep  9 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-6
+- Rebuild for ocaml-ocamlgraph 2.1.0
+
+* Sat Jul 29 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-5
+- Require cvc5 instead of cvc4
+
+* Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-4
+- Rebuild for ocaml-zarith 1.13
+
+* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 1.6.0-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
+
+* Tue Jul 18 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-2
+- Validate metadata with appstream-util
+
+* Thu Jul 13 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-2
+- Rebuild for mpfr 4.2.0
+
+* Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-1
+- Version 1.6.0
+- Enable inference with BDDs
+- Add patch for coq 8.17 support
+
+* Sat Apr  1 2023 Jerry James <loganjerry@gmail.com> - 1.5.1-7
+- Rebuild for coq 8.17.0
+
+* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 1.5.1-6
+- Rebuild OCaml packages for F38
+
+* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 1.5.1-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
+
+* Fri Jan  6 2023 Jerry James <loganjerry@gmail.com> - 1.5.1-4
+- BR tex(tgtermes.sty) to fix FTBFS with TeXLive 2022
+
+* Sat Nov 26 2022 Jerry James <loganjerry@gmail.com> - 1.5.1-3
+- Rebuild for coq 8.16.1
+
+* Tue Nov  1 2022 Jerry James <loganjerry@gmail.com> - 1.5.1-2
+- Rebuild for ocaml-ppxlib 0.28.0
+
+* Fri Sep 16 2022 Jerry James <loganjerry@gmail.com> - 1.5.1-1
+- Version 1.5.1
+
+* Thu Aug 18 2022 Jerry James <loganjerry@gmail.com> - 1.5.0-3
+- Rebuild to fix coq dependency
+- Convert License tag to SPDX
+
+* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 1.5.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
+
+* Tue Jul 19 2022 Jerry James <loganjerry@gmail.com> - 1.5.0-1
+- Remove i686 support
+
+* Thu Jul  7 2022 Jerry James <loganjerry@gmail.com> - 1.5.0-1
+- Version 1.5.0
+- Add ocaml-mlmpfr support
+- Drop unmaintained man pages
+- Use new OCaml macros
+
+* Sun Jun 19 2022 Richard W.M. Jones <rjones@redhat.com> - 1.4.1-3
+- OCaml 4.14.0 rebuild
+
+* Fri Mar 25 2022 Jerry James <loganjerry@gmail.com> - 1.4.1-2
+- Rebuild for coq 8.15.1
+
+* Mon Feb 28 2022 Jerry James <loganjerry@gmail.com> - 1.4.1-1
+- Version 1.4.1
+
+* Fri Feb 04 2022 Richard W.M. Jones <rjones@redhat.com> - 1.4.0-11
+- OCaml 4.13.1 rebuild to remove package notes
+
+* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 1.4.0-10
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
+
+* Mon Jan 17 2022 Jerry James <loganjerry@gmail.com> - 1.4.0-9
+- Rebuild for menhir 20211230
+
+* Mon Dec 27 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-8
+- Rebuild for alt-ergo 2.3.0 and ocaml-zip 1.11
+
+* Tue Nov 30 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-7
+- Rebuild for coq 8.14.1, sexplib0 0.15.0 and menhir 20211128
+
+* Thu Oct 21 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-6
+- Rebuild for coq 8.14.0 and menhir 20211012
+- Add -coq8.14 patch
+- Drop XEmacs support
+
+* Tue Oct 05 2021 Richard W.M. Jones <rjones@redhat.com> - 1.4.0-5
+- OCaml 4.13.1 build
+
+* Mon Oct 04 2021 Richard W.M. Jones <rjones@redhat.com> - 1.4.0-4
+- Try to build on s390x with OCaml 4.13
+
+* Fri Jul 30 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-3
+- Rebuild for rebuilt coq
+
+* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 1.4.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
+
+* Wed Jul 14 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-1
+- Version 1.4.0
+- Drop all patches
+- Validate with appstreamcli instead of appstream-util
+
+* Tue Jun  8 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-9
+- Rebuild for ocaml-menhir 20210419
+
+* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-8
+- Rebuild for coq 8.13.1 and ocaml-zarith 1.12
+
+* Tue Mar  2 11:18:12 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 1.3.3-7
+- OCaml 4.12.0 build
+
+* Sat Feb 20 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-6
+- Rebuild for coq 8.13.0
+- Update metainfo and install in metainfodir
+
+* Wed Jan 27 2021 Fedora Release Engineering <releng@fedoraproject.org> - 1.3.3-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
+
+* Sat Jan  2 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-4
+- Rebuild for flocq 3.4.0
+
+* Wed Dec 23 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-3
+- Rebuild for coq 8.12.2
+
+* Wed Dec  2 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-2
+- Rebuild for coq 8.12.1 and menhir 20201201
+
+* Fri Sep 25 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-1
+- Version 1.3.3
+
+* Wed Sep 02 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-14
+- OCaml 4.11.1 rebuild
+
+* Tue Sep  1 2020  Jerry James <loganjerry@gmail.com> - 1.3.1-13
+- Rebuild for coq 8.12.0
+
+* Mon Aug 24 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-13
+- OCaml 4.11.0 rebuild
+
+* Thu Aug  6 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-12
+- Rebuild for ocaml-lablgtk3 3.1.1 and ocaml-menhir 20200624
+
+* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 1.3.1-11
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
+
+* Mon Jun 15 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-10
+- Rebuild for coq 8.11.2
+
+* Sat Jun 13 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-9
+- Rebuild for flocq 3.3.1
+- Build the coq files with the native compiler when possible
+
+* Wed May 20 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-8
+- Rebuild for coq 8.11.1
+
+* Tue May 05 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-7
+- OCaml 4.11.0+dev2-2020-04-22 rebuild
+
+* Sun Apr 12 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-6
+- Make the dependencies on ocaml-num and ocaml-zip explicit (bz 1795083)
+
+* Wed Apr  8 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-5
+- Rebuild for flocq 3.2.1
+
+* Sun Apr 05 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-4
+- Update all OCaml dependencies for RPM 4.16.
+
+* Wed Apr  1 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-3
+- Do not build with mlmpfr; symbols clash with mlgmpidl, causing frama-c to
+  fail to start
+- Obsolete the why2 packages
+
+* Sat Mar 28 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-2
+- Remove useless BRs and Rs (bz 1817878)
+
+* Wed Mar 25 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-1
+- Version 1.3.1
+
+* Fri Jan 31 2020 Fedora Release Engineering <releng@fedoraproject.org> - 1.2.1-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
+
+* Wed Jan 22 2020 Jerry James <loganjerry@gmail.com> - 1.2.1-3
+- OCaml 4.10.0+beta1 rebuild.
+
+* Fri Dec 06 2019 Richard W.M. Jones <rjones@redhat.com> - 1.2.1-2
+- OCaml 4.09.0 (final) rebuild.
+
+* Tue Oct 29 2019 Jerry James <loganjerry@gmail.com> - 1.2.1-1
+- New upstream release
+- Add -proofgeneral subpackage
+- Add desktop and AppData files
+
+* Fri Oct 11 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-6
+- Rebuild for ocaml-menhir 20190924
+
+* Fri Sep  6 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-5
+- Rebuild for ocaml-zarith 1.9
+
+* Thu Aug  1 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-4
+- Also install the library, for consumption by frama-c
+
+* Thu Aug  1 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-3
+- Rebuild for flocq 3.2.0
+
+* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.2.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
+
+* Wed Jun  5 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-1
+- New upstream release
+
+* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.1.1-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
+
+* Sat Jan 26 2019 Jerry James <loganjerry@gmail.com> - 1.1.1-1
+- New upstream release
+
+* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.88.3-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
+
+* Thu Jul 12 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-4
+- OCaml 4.07.0 (final) rebuild.
+
+* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-3
+- Bump release and rebuild.
+
+* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-2
+- OCaml 4.07.0-rc1 rebuild.
+
+* Mon Feb 12 2018 Jerry James <loganjerry@gmail.com> - 0.88.3-1
+- New upstream release
+
+* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.88.2-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
+
+* Sat Dec  9 2017 Jerry James <loganjerry@gmail.com> - 0.88.2-1
+- New upstream release
+
+* Fri Nov 17 2017 Richard W.M. Jones <rjones@redhat.com> - 0.88.1-1
+- New upstream version 0.88.1.
+- OCaml 4.06.0 rebuild.
+
+* Sat Oct  7 2017 Jerry James <loganjerry@gmail.com> - 0.88.0-1
+- New usptream release
+
+* Thu Oct  5 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-12
+- Rebuild for flocq 2.6.0
+
+* Wed Sep 06 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-11
+- OCaml 4.05.0 rebuild.
+
+* Thu Aug 03 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-10
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
+
+* Thu Jul 27 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-9
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
+
+* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-8
+- Bump release and rebuild.
+
+* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-7
+- Bump release and rebuild.
+
+* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-6
+- Bump release and rebuild.
+
+* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-5
+- OCaml 4.04.2 rebuild.
+
+* Fri May 12 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-4
+- OCaml 4.04.1 rebuild.
+
+* Fri Mar 24 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-3
+- Rebuild to fix coq consistency issue
+
+* Sat Feb 11 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
+
+* Thu Jan 12 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-1
+- New upstream release
+
+* Mon Nov 07 2016 Richard W.M. Jones <rjones@redhat.com> - 0.87.2-4
+- Rebuild for OCaml 4.04.0.
+
+* Fri Oct 28 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-3
+- Rebuild for coq 8.5pl3
+- Remove obsolete scriptlets
+- Fix install location of why3lang.sty
+
+* Thu Sep 29 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-2
+- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1
+
+* Fri Sep  2 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-1
+- New upstream release
+
+* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 0.87.1-2
+- Rebuild for coq 8.5pl2
+
+* Wed Jun  1 2016 Jerry James <loganjerry@gmail.com> - 0.87.1-1
+- New upstream release
+
+* Fri Apr 22 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-3
+- Rebuild for coq 8.5pl1
+
+* Sat Apr 16 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-2
+- Rebuild for ocaml-ocamlgraph 1.8.7
+
+* Fri Mar 18 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-1
+- New upstream release
+- Drop boomy icon removal; upstream no longer ships them
+
+* Fri Feb 12 2016 Jerry James <loganjerry@gmail.com> - 0.86.3-1
+- New upstream release
+- Use camlp4 in preference to camlp5
+
+* Fri Feb 05 2016 Fedora Release Engineering <releng@fedoraproject.org> - 0.86.2-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
+
+* Wed Nov 25 2015 Jerry James <loganjerry@gmail.com> - 0.86.2-2
+- Rebuild for ocaml-zarith 1.4.1 and ocaml-menhir 20151112
+
+* Wed Oct 14 2015 Jerry James <loganjerry@gmail.com> - 0.86.2-1
+- New upstream release
+- Do not ship the nonfree boomy icons
+
+* Wed Jun 24 2015 Richard W.M. Jones <rjones@redhat.com> - 0.86.1-2
+- ocaml-4.02.2 final rebuild.
+
+* Mon Jun 22 2015 Jerry James <loganjerry@gmail.com> - 0.86.1-1
+- New upstream release
+
+* Wed Jun 17 2015 Richard W.M. Jones <rjones@redhat.com> - 0.86-2
+- ocaml-4.02.2 rebuild.
+
+* Sat May 16 2015 Jerry James <loganjerry@gmail.com> - 0.86-1
+- New upstream release
+
+* Sat Apr 11 2015 Jerry James <loganjerry@gmail.com> - 0.85-9
+- Rebuild for coq 8.4pl6
+
+* Wed Mar 18 2015 Jerry James <loganjerry@gmail.com> - 0.85-8
+- Rebuild for ocaml-ocamlgraph 1.8.6
+
+* Sat Feb 21 2015 Jerry James <loganjerry@gmail.com> - 0.85-7
+- Note bundled jquery
+- Fix sed expression separators for new RPM_OPT_FLAGS and RPM_LD_FLAGS
+
+* Wed Feb 18 2015 Richard W.M. Jones <rjones@redhat.com> - 0.85-6
+- ocaml-4.02.1 rebuild.
+
+* Thu Nov  6 2014 Jerry James <loganjerry@gmail.com> - 0.85-5
+- Rebuild for ocaml-camlp5 6.12
+
+* Thu Oct 30 2014 Jerry James <loganjerry@gmail.com> - 0.85-4
+- Rebuild for coq 8.4pl5
+
+* Tue Oct 14 2014 Jerry James <loganjerry@gmail.com> - 0.85-3
+- Rebuild for ocaml-zarith 1.3
+
+* Thu Sep 18 2014 Jerry James <loganjerry@gmail.com> - 0.85-2
+- Bump and rebuild
+
+* Wed Sep 17 2014 Jerry James <loganjerry@gmail.com> - 0.85-1
+- New upstream release
+- New source URL
+
+* Tue Sep  2 2014 Jerry James <loganjerry@gmail.com> - 0.84-1
+- New upstream release
+- Fix license handling
+
+* Mon Aug 25 2014 Jerry James <loganjerry@gmail.com> - 0.83-14
+- Rebuild for new gappalib-coq build
+
+* Sun Aug 24 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-13
+- ocaml-4.02.0+rc1 rebuild.
+
+* Mon Aug 18 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.83-12
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
+
+* Mon Aug  4 2014 Jerry James <loganjerry@gmail.com> - 0.83-11
+- Rebuild for new gappalib-coq build
+
+* Sat Aug 02 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-10
+- ocaml-4.02.0-0.8.git10e45753.fc22 rebuild.
+
+* Fri Aug 01 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-9
+- OCaml 4.02.0 beta rebuild.
+
+* Thu Jun 26 2014 Jerry James <loganjerry@gmail.com> - 0.83-8
+- Linking with -z relro -z now breaks plugins; omit "-z now"
+
+* Sun Jun 08 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.83-7
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
+
+* Tue May 13 2014 Jerry James <loganjerry@gmail.com> - 0.83-6
+- Rebuild for coq 8.4pl4
+
+* Mon Apr 21 2014 Jerry James <loganjerry@gmail.com> - 0.83-5
+- Rebuild for flocq 2.3.0 and ocamlgraph 1.8.5
+- Drop unnecessary sqlite-devel BR
+
+* Tue Apr 15 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-4
+- Remove ocaml_arches macro (RHBZ#1087794).
+
+* Mon Mar 24 2014 Jerry James <loganjerry@gmail.com> - 0.83-3
+- Apply upstream fix for building with ocaml-zarith
+- Fix file encodings
+- Fix permission bits
+
+* Tue Mar 18 2014 Jerry James <loganjerry@gmail.com> - 0.83-2
+- Back out the post-release fix to the Coq printer, which breaks Frama-C
+
+* Fri Mar 14 2014 Jerry James <loganjerry@gmail.com> - 0.83-1
+- New upstream release
+- Use cvc4 instead of cvc3
+
+* Wed Feb 26 2014 Jerry James <loganjerry@gmail.com> - 0.82-2
+- Rebuild for ocamlgraph 1.8.4
+- BR ocaml-findlib instead of ocaml-findlib-devel
+
+* Fri Dec 13 2013 Jerry James <loganjerry@gmail.com> - 0.82-1
+- New upstream release
+- Drop upstreamed patches
+- Add -examples subpackage
+- Install LaTeX style
+- Turn off frama-c support at upstream's request
+
+* Mon Sep 30 2013 Jerry James <loganjerry@gmail.com> - 0.81-6
+- Apply upstream fix for change in the alt-ergo timelimit option
+
+* Tue Sep 17 2013 Jerry James <loganjerry@gmail.com> - 0.81-5
+- Rebuild for OCaml 4.01.0
+- Enable debuginfo for the ocaml sources
+
+* Sun Aug 04 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.81-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
+
+* Fri Jun 21 2013 Jerry James <loganjerry@gmail.com> - 0.81-3
+- Rebuild for frama-c Fluorine 20130601
+
+* Thu May 23 2013 Jerry James <loganjerry@gmail.com> - 0.81-2
+- Rebuild for frama-c Fluorine 20130501
+
+* Fri May 10 2013 Jerry James <loganjerry@gmail.com> - 0.81-1
+- New upstream release
+- Disable PVS support for now; it requires the NASA libraries
+- Fix the conflict between the why and why3 Emacs packages (bz 913522)
+- Disable parallel builds due to intermittent build failures
+
+* Fri Feb 15 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.73-5
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
+
+* Mon Jan  7 2013 Jerry James <loganjerry@gmail.com> - 0.73-4
+- Rebuild for coq 8.4pl1
+
+* Fri Dec 14 2012 Richard W.M. Jones <rjones@redhat.com> - 0.73-3
+- Rebuild for OCaml 4.00.1.
+
+* Thu Aug 23 2012 Jerry James <loganjerry@gmail.com> - 0.73-2
+- Rebuild for coq 8.4
+
+* Thu Aug  2 2012 Jerry James <loganjerry@gmail.com> - 0.73-1
+- New upstream release
+
+* Sun Jul 22 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.71-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
+
+* Thu Apr 19 2012 Jerry James <loganjerry@gmail.com> - 0.71-2
+- Add missing sqlite-devel BR
+- Do not move the coq plugin
+- Generate debuginfo for the sole C program
+- Add man pages
+
+* Fri Dec 16 2011 Jerry James <loganjerry@gmail.com> - 0.71-1
+- Initial RPM
--- a/2
+++ b/2
@ -1 +1 @@
-SHA512 (why3-1.6.0.tar.gz) = 60d61b8337ab9f2fd2e6c7174eb0bab063f122417738cd75990c5c53120dd535bcedccb670567f5753853d6bc9f8efebb563d079e4d368372a7687193f1346b1
+SHA512 (why3-1.8.2.tar.gz) = a35e88fafe1aa29c36d2248c1a644eae85afa1bb7b3009193f4a5c28ba684d0882717d63733d8581a7c2cd5ec493e2d15c82baabef615b4d00323fa9309875f8
--- a/why3-coq-8.17.patch
+++ b/why3-coq-8.17.patch
@ -1,82 +0,0 @@
--- why3-1.6.0/configure.in.orig	2023-03-07 02:15:31.000000000 -0700
-+++ why3-1.6.0/configure.in	2023-06-26 14:21:56.361457115 -0600
-@@ -993,6 +993,10 @@ if test "$enable_coq_support" = yes; the
-       8.16*)
-          coq_compat_version="COQ816"
-          ;;
-+      8.17*)
-+         coq_compat_version="COQ817"
-+         COQFLAGS="-w deprecated-instance-without-locality,deprecated-hint-without-locality"
-+         ;;
-       *)
-          enable_coq_support=no
-          AC_MSG_WARN([You need Coq 8.7 or later; Coq discarded.])
-@@ -1242,6 +1246,7 @@ AC_SUBST(COQC)
- AC_SUBST(COQDEP)
- AC_SUBST(COQLIB)
- AC_SUBST(COQVERSION)
-+AC_SUBST(COQFLAGS)
- 
- AC_SUBST(enable_pvs_libs)
- AC_SUBST(PVS)
--- why3-1.6.0/configure.orig	2023-03-07 02:15:31.000000000 -0700
-+++ why3-1.6.0/configure	2023-06-26 14:35:07.856280739 -0600
-@@ -696,6 +696,7 @@ PVSVERSION
- enable_pvs_libs
- COQVERSION
- COQLIB
-+COQFLAGS
- coq_compat_version
- enable_coq_fp_libs
- enable_coq_libs
-@@ -5926,6 +5927,10 @@ printf "%s\n" "$COQVERSION" >&6; }
-       8.16*)
-          coq_compat_version="COQ816"
-          ;;
-+      8.17*)
-+         coq_compat_version="COQ817"
-+         COQFLAGS="-w deprecated-instance-without-locality,deprecated-hint-without-locality"
-+         ;;
-       *)
-          enable_coq_support=no
-          { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: You need Coq 8.7 or later; Coq discarded." >&5
--- why3-1.6.0/Makefile.in.orig	2023-03-07 02:15:31.000000000 -0700
-+++ why3-1.6.0/Makefile.in	2023-06-26 14:21:12.426061732 -0600
-@@ -62,6 +62,7 @@ OCAMLBEST = @OCAMLBEST@
- OCAMLVERSION = @OCAMLVERSION@
- COQC      = @COQC@
- COQDEP    = @COQDEP@
-+COQFLAGS  = @COQFLAGS@
- FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
- MENHIR	  = @MENHIR@
- 
-@@ -1068,7 +1069,7 @@ COQLIBS_FILES = lib/coq/BuiltIn lib/coq/
- 
- %.vo: %.v
- 	$(SHOW) 'Coqc     $<'
-	$(HIDE)$(COQC) -R lib/coq Why3 $<
-+	$(HIDE)$(COQC) $(COQFLAGS) -R lib/coq Why3 $<
- 
- %.vd: %.v
- 	$(SHOW) 'Coqdep   $<'
--- why3-1.6.0/share/provers-detection-data.conf.orig	2023-03-07 02:15:31.000000000 -0700
-+++ why3-1.6.0/share/provers-detection-data.conf	2023-06-26 14:22:52.768680868 -0600
-@@ -838,16 +838,8 @@ support_library = "%l/coq/version"
- exec = "coqtop"
- version_switch = "-v"
- version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
-version_ok = "^8\.16\.[0-9]+$"
-version_ok = "^8\.15\.[0-9]+$"
-version_ok = "^8\.14\.[0-9]+$"
-version_ok = "^8\.13\.[0-9]+$"
-version_ok = "^8\.12\.[0-9]+$"
-version_ok = "^8\.11\.[0-9]+$"
-version_ok = "^8\.10\.[0-9]+$"
-version_ok = "^8\.9\.[0-9]+$"
-version_ok = "^8\.8\.[0-9]+$"
-version_ok = "^8\.7\.[0-9]+$"
-+version_ok = "^8\.1[0-7]\.[0-9]+$"
-+version_ok = "^8\.[7-9]\.[0-9]+$"
- version_old = "8.6.1"
- version_old = "8.6"
- version_old = "^8\.5pl[1-3]$"
--- a/why3-rocq-9.2.patch
+++ b/why3-rocq-9.2.patch
@ -0,0 +1,292 @@
+--- why3-1.8.2/lib/coq/ieee_float/GenericFloat.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/ieee_float/GenericFloat.v	2026-04-12 21:00:50.656964191 -0600
+@@ -476,7 +476,7 @@ Qed.
+ 
+ Lemma is_nan_dec: forall x, {is_nan x} + {~ is_nan x}.
+ Proof.
+-  intro; destruct x; compute; intuition.
+  intro; destruct x; compute; intuition; auto with *.
+ Qed.
+ 
+ Lemma eq_not_nan_refl: forall {x : t}, ~ is_nan x -> eq x x.
+--- why3-1.8.2/lib/coq/map/Occ.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/map/Occ.v	2026-04-12 20:11:22.595468204 -0600
+@@ -241,10 +241,10 @@ now rewrite occ_empty; lia.
+ destruct (why_decidable_eq (m (l + (x-1))%Z) v).
+ assert (m (l + (x - 1)) <> v)%Z.
+   apply H1; lia.
+-intuition.
+intuition; auto with *.
+ rewrite occ_right_no_add.
+ replace (l+x-1)%Z with (l+(x-1))%Z by ring.
+-apply H; intuition.
+apply H; intuition; auto with *.
+ apply (H1 i). lia. assumption.
+ lia.
+ replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
+--- why3-1.8.2/lib/coq/number/Prime.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/number/Prime.v	2026-04-11 14:50:08.453344009 -0600
+@@ -34,6 +34,8 @@ intros p.
+ apply iff_trans with (2 := prime_alt p).
+ unfold prime, prime'.
+ intuition.
+lia.
+lia.
+ Qed.
+ 
+ (* Why3 goal *)
+--- why3-1.8.2/lib/coq/set/Cardinal.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/set/Cardinal.v	2026-04-11 20:38:44.347517956 -0600
+@@ -165,9 +165,10 @@ destruct (Bool.bool_dec (s x) true) as [
+ + exists (List.cons x l1).
+   split.
+   - constructor; auto. intro Habs. eapply h1 in Habs. unfold Map.set in Habs. 
+-    destruct why_decidable_eq; intuition.
+    destruct why_decidable_eq; auto with *.
+   - unfold Map.set in h1. intros. specialize (h1 e). destruct why_decidable_eq; [| intuition]. subst.
+-    split; intuition. destruct H1; eauto.
+    split; auto with *. destruct H1; eauto.
+    auto with *.
+ + exists l1.
+   split; [auto|]. intros. specialize (h1 e). replace (Map.set s x false e) with (s e) in h1.
+   eauto.
+@@ -184,12 +185,15 @@ induction l.
+ - destruct IHl. destruct H.
+   destruct (List.in_dec eq_dec a l). 
+   + exists x. split; eauto. intros. rewrite H0.
+-    split; intuition. inversion H2; eauto. subst. assumption.
+    split; auto with *; intuition. apply List.in_cons. assumption.
+    inversion H2; eauto. subst. assumption.
+   + destruct (Pdec a). 
+     ++ exists (List.cons a x). split. constructor; eauto.
+        rewrite H0. intro Habs. destruct Habs; eauto.
+        intros. simpl. rewrite H0. intuition. subst. assumption.
+-    ++ exists x. split; eauto. intros. rewrite H0. intuition. simpl in H2. destruct H2; try subst; intuition. 
+    ++ exists x. split; eauto. intros. rewrite H0. auto with *; intuition.
+       apply List.in_cons. assumption.
+       simpl in H2. destruct H2; try subst; intuition. 
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -443,7 +447,7 @@ split; intros.
+       + eapply List.NoDup_incl_length; eauto. apply a0. intros e Hincl. eapply H2. assumption.
+       + eapply List.NoDup_incl_length; eauto. intros e Hincl. eapply H2. assumption.
+     }
+-    intuition.
+    intuition. auto with *.
+   }
+   rewrite Hnat. rewrite Nat2Z.inj_succ. ring. 
+ Qed.
+@@ -472,6 +476,7 @@ split.
+   assert (~ set.Set.mem x s'). 
+   { unfold s'. unfold Map.set, set.Set.mem.
+     destruct why_decidable_eq; intuition. 
+    discriminate H1.
+   }
+   eapply cardinal_add in H1. rewrite H1. ring.
+   unfold s'. eapply is_finite_remove. assumption.
+--- why3-1.8.2/lib/coq/set/FsetInt.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/set/FsetInt.v	2026-04-12 12:49:09.882660225 -0600
+@@ -127,8 +127,8 @@ Fixpoint seqZ l len : list Numbers.BinNu
+ 
+ Lemma seqZ_le: forall len x l, List.In x (seqZ l len) -> (l <= x)%Z.
+ Proof.
+-induction len; simpl; intuition.
+-eapply IHlen in H0; intuition.
+induction len; simpl; intuition. auto with *.
+eapply IHlen in H0; intuition. auto with *.
+ Qed.
+ 
+ Lemma seqZ_le2: forall len x l, List.In x (seqZ l len) -> (x < l + Z.of_nat len)%Z.
+@@ -184,8 +184,9 @@ destruct (Z_le_dec l r).
+     destruct Z_le_dec.
+     * destruct Z_lt_dec. split; intros; [reflexivity|].
+       intuition.
+-      intuition ; try inversion H.
+-    * intuition ; try inversion H.
+      intuition ; auto with *; try inversion H.
+      intuition ; auto with *; try inversion H.
+    * intuition ; auto with *; try inversion H.
+ + exists List.nil. 
+   split.
+   - constructor.
+@@ -230,9 +231,10 @@ destruct (Z_le_dec l r).
+   split. apply seqZ_NoDup.
+   intros. rewrite seqZ_In_iff.
+   rewrite Z2Nat.id; [|lia].
+-  destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H.
+  destruct Z_le_dec; try destruct Z_lt_dec; intuition; auto with *; try inversion H.
+ + exists nil. split. constructor.
+   simpl. intros. destruct Z_le_dec; try destruct Z_lt_dec; intuition.
+  auto with *. auto with *. auto with *.
+ Qed.
+ 
+ 
+@@ -265,6 +267,6 @@ split.
+ + intros. destruct a. 
+   destruct x. reflexivity.
+   specialize (H2 z). contradict H2. destruct Z_le_dec. 
+-  destruct Z_lt_dec. lia. intuition. intuition.
+  destruct Z_lt_dec. lia. intuition; auto with *. intuition; auto with *.
+ Qed.
+ 
+--- why3-1.8.2/lib/coq/set/FsetSum.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/set/FsetSum.v	2026-04-12 13:20:34.237382880 -0600
+@@ -101,8 +101,8 @@ destruct ClassicalEpsilon.constructive_i
+ destruct a0 as (Hx0dup, Hx0eq). destruct a1 as (Hx1dup, Hx1eq).
+ split. intros.
+ + eapply fold_left_iff_symm; eauto.
+-  * intuition.
+-  * intuition.
+  * intuition; auto with *.
+  * intuition; auto with *.
+   * intros. rewrite Hx0eq. rewrite Hx1eq. unfold Map.set. 
+     destruct why_decidable_eq; try subst; intuition.
+ + intros.
+@@ -113,19 +113,19 @@ split. intros.
+   erewrite <- (fold_left_iff_symm (List.app x0' x0'')); eauto.
+   * rewrite List.fold_left_app. rewrite fold_left_symm.
+     ++ auto.
+-    ++ intuition.
+-    ++ intuition.
+-  * intuition.
+-  * intuition.
+    ++ intuition; auto with *.
+    ++ intuition; auto with *.
+  * intuition; auto with *.
+  * intuition; auto with *.
+   * intros. rewrite List.in_app_iff. rewrite Hx0 in Hx0eq.
+     specialize (Hx0eq e). rewrite List.in_app_iff in Hx0eq. simpl in Hx0eq.
+     unfold Map.set in *. split; intros.
+     ++ destruct H2.
+        ** apply Hx1eq. destruct why_decidable_eq.
+-          -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition.
+          -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition; auto with *.
+           -- intuition.
+        ** eapply Hx1eq. destruct why_decidable_eq.
+-          -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition.
+          -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition; auto with *.
+           -- intuition.
+     ++ eapply Hx1eq in H2.
+        destruct why_decidable_eq.
+@@ -177,11 +177,11 @@ destruct ClassicalEpsilon.constructive_i
+ destruct a1 as (Hdidup, Hdieq).
+ destruct a0 as (Hx0dup, Hx0eq).
+ destruct a2 as (Hx1dup, Hx1eq).
+-  rewrite fold_left_symm; try now intuition.
+  rewrite fold_left_symm; try now intuition; auto with *.
+   rewrite Z.add_0_l. rewrite <- List.fold_left_app.
+   eapply fold_left_iff_symm; eauto.
+-  + intuition.
+-  + intuition.
+  + intuition; auto with *.
+  + intuition; auto with *.
+   + intros. rewrite List.in_app_iff. rewrite Hx1eq. rewrite Hx0eq.
+     rewrite Hdieq. rewrite set.Set.diff'def. unfold set.Set.mem.
+     split; intros.
+@@ -210,11 +210,11 @@ destruct ClassicalEpsilon.constructive_i
+ destruct a0 as (Hundup, Huneq).
+ destruct a1 as (Hx0dup, Hx0eq).
+ destruct a2 as (Hx1dup, Hx1eq).
+-  rewrite fold_left_symm; try now intuition.
+  rewrite fold_left_symm; try now intuition; auto with *.
+   rewrite Z.add_0_l. rewrite <- List.fold_left_app.
+   eapply fold_left_iff_symm; eauto.
+-  + intuition.
+-  + intuition.
+  + intuition; auto with *.
+  + intuition; auto with *.
+   + intros. rewrite List.in_app_iff. rewrite Hx1eq. rewrite Hx0eq. rewrite Huneq.
+     rewrite set.Set.union'def. clear - e. intuition.
+   + eapply Cardinal.NoDup_app; eauto.
+@@ -312,7 +312,7 @@ assert (Z.of_nat (length (a0 :: x)) = Z.
+ simpl. rewrite Zpos_P_of_succ_nat. ring.
+ rewrite H.
+ rewrite IHx. rewrite @fold_left_symm; eauto.
+-intuition.
+-intuition.
+intuition; auto with *.
+intuition; auto with *.
+ Qed.
+ 
+--- why3-1.8.2/lib/coq/set/Fset.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/set/Fset.v	2026-04-11 21:14:24.563998083 -0600
+@@ -103,12 +103,14 @@ Proof.
+ exists (fun x => false). 
+ apply Cardinal.is_finite_empty. unfold set.Set.is_empty.
+ unfold set.Set.mem. intuition.
+discriminate H.
+ Defined.
+ 
+ (* Why3 goal *)
+ Lemma is_empty_empty {a:Type} {a_WT:WhyType a} : is_empty (empty : fset a).
+ Proof.
+ unfold empty, is_empty, mem, set.Set.mem. intuition.
+discriminate H.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -118,6 +120,7 @@ Proof.
+ intros s h1.
+ eapply extensionality. intro. unfold empty, is_empty, mem, set.Set.mem in *.
+ destruct s. intuition. destruct (h1 _ H). 
+discriminate H.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -163,6 +166,7 @@ Proof.
+ intros x s y.
+ unfold mem, remove, set.Set.mem, Map.set. destruct s.
+ destruct why_decidable_eq; intuition.
+discriminate H. discriminate H.
+ Qed.
+ 
+ (* Why3 goal *)
+--- why3-1.8.2/lib/coq/set/SetImpInt.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/set/SetImpInt.v	2026-04-12 13:35:37.131334141 -0600
+@@ -48,6 +48,6 @@ Lemma choose'spec :
+ Proof.
+ intros s h1.
+ destruct h1. unfold to_fset, Fset.is_empty, Fset.mem, set.Set.mem.
+-intuition.
+intuition. inversion H.
+ Qed.
+ 
+--- why3-1.8.2/lib/coq/set/SetImp.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/set/SetImp.v	2026-04-12 13:28:53.584021692 -0600
+@@ -53,6 +53,6 @@ Lemma choose'spec :
+ Proof.
+ intros s h1.
+ destruct h1. unfold to_fset, Fset.is_empty, Fset.mem, set.Set.mem.
+-intuition.
+intuition. inversion H.
+ Qed.
+ 
+--- why3-1.8.2/lib/coq/set/Set.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/set/Set.v	2026-04-11 15:34:29.297022916 -0600
+@@ -139,6 +139,7 @@ Proof.
+ intros x s y.
+ unfold mem, Map.set.
+ destruct (why_decidable_eq x y) as [->|H] ; intuition.
+discriminate H.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -332,7 +333,7 @@ intuition.
+   destruct (s1 x); destruct (s2 x); intuition.
+ - rewrite <- H.
+   rewrite Bool.andb_true_iff.
+-  destruct (s2 x); intuition.
+  destruct (s2 x); auto with *.
+ Qed.
+ 
+ (* Why3 goal *)
+@@ -345,7 +346,7 @@ unfold disjoint, diff.
+ unfold mem.
+ intros x.
+ rewrite Bool.andb_true_iff.
+-destruct (s2 x); intuition.
+destruct (s2 x); auto with *.
+ Qed.
+ 
+ (* Why3 goal *)
--- a/why3-zmod.patch
+++ b/why3-zmod.patch
@ -0,0 +1,33 @@
+--- why3-1.8.2/lib/coq/bv/BV_Gen.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/bv/BV_Gen.v	2026-03-03 17:07:31.885655859 -0700
+@@ -994,7 +994,7 @@ match p with
+             ((Vector.last prev) :: (Vector.shiftout prev))
+ end.
+ 
+-Lemma mod1_is_mod : forall x y, y > 0 -> mod1 x y = Zmod x y.
+Lemma mod1_is_mod : forall x y, y > 0 -> mod1 x y = Z.modulo x y.
+   intros; unfold mod1, div.
+   case Z_le_dec; intro.
+   rewrite Z.mod_eq by lia; trivial.
+--- why3-1.8.2/lib/coq/int/EuclideanDivision.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/int/EuclideanDivision.v	2026-03-03 17:08:16.588687381 -0700
+@@ -21,7 +21,7 @@ Require Import Lia.
+ Definition div : Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
+ Proof.
+ intros x y.
+-case (Z_le_dec 0 (Zmod x y)) ; intros H.
+case (Z_le_dec 0 (Z.modulo x y)) ; intros H.
+ exact (Z.div x y).
+ exact (Z.div x y + 1)%Z.
+ Defined.
+--- why3-1.8.2/lib/coq/number/Divisibility.v.orig	2025-09-16 09:37:32.000000000 -0600
+++ why3-1.8.2/lib/coq/number/Divisibility.v	2026-03-03 17:08:33.884500190 -0700
+@@ -203,7 +203,7 @@ Lemma divides_mod_euclidean :
+   divides b a -> ((int.EuclideanDivision.mod1 a b) = 0%Z).
+ Proof.
+ intros a b Zb H.
+-assert (Zmod a b = Z0).
+assert (Z.modulo a b = Z0).
+ now apply Zdivide_mod.
+ unfold mod1, div.
+ rewrite H0.
--- a/why3.spec
+++ b/why3.spec
@ -1,43 +1,34 @@
-# Coq's plugin architecture requires cmxs files, so:
-ExclusiveArch: %{ocaml_native_compiler}
-
-# ANTLR is unavailable on i686, so coq is also unavailable.  We could build
-# without coq support, but choose to forgo i686 support entirely.
-# See https://fedoraproject.org/wiki/Changes/Drop_i686_JDKs
-# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
-#ExclusiveArch:  %%{java_arches}
-
 # NOTE: Upstream has said that the Frama-C support is still experimental, and
 # less functional than the corresponding support in why2.  They recommend not
 # enabling it for now.  We abide by their wishes.  Revisit this decision each
 # release.

-%ifnarch %{ocaml_native_compiler}
-%global debug_package %{nil}
-%endif
-
 Name:           why3
-Version:        1.6.0
-Release:        6%{?dist}
+Version:        1.8.2
+Release:        %autorelease
 Summary:        Software verification platform

 License:        LGPL-2.1-only WITH OCaml-LGPL-linking-exception
-URL:            https://why3.lri.fr/
+URL:            https://www.why3.org/
+VCS:            git:https://gitlab.inria.fr/why3/why3.git
 Source0:        https://why3.gitlabpages.inria.fr/releases/%{name}-%{version}.tar.gz
 # Desktop file written by Jerry James
 Source1:        fr.lri.%{name}.desktop
 # AppData file written by Jerry James
 Source2:        fr.lri.%{name}.metainfo.xml
+# The deprecated Zmod alias was removed in rocq-stdlib 9.1.0
+Patch:          %{name}-zmod.patch
+# Adapt to changes in rocq 9.2.0
+Patch:          %{name}-rocq-9.2.patch

-# Support coq 8.17.  See
-# https://gitlab.inria.fr/why3/why3/-/commit/64facc03bdc2bc4ce0586ff2f458bcd87f646ba8
-Patch0:         %{name}-coq-8.17.patch
+# Coq's plugin architecture requires cmxs files, so:
+ExclusiveArch:  %{ocaml_native_compiler}

-BuildRequires:  coq
-BuildRequires:  emacs-nox
+BuildRequires:  coq-core-compat
+BuildRequires:  emacs-nw
 BuildRequires:  emacs-proofgeneral
 BuildRequires:  flocq
-BuildRequires:  graphviz
+BuildRequires:  java-devel
 BuildRequires:  latexmk
 BuildRequires:  libappstream-glib
 BuildRequires:  make
@ -49,7 +40,6 @@ BuildRequires:  ocaml-lablgtk3-sourceview3-devel
 BuildRequires:  ocaml-menhir
 BuildRequires:  ocaml-mlmpfr-devel
 BuildRequires:  ocaml-num-devel
-BuildRequires:  ocaml-ocamldoc
 BuildRequires:  ocaml-ocamlgraph-devel
 BuildRequires:  ocaml-ppx-deriving-devel
 BuildRequires:  ocaml-ppx-sexp-conv-devel
@ -57,19 +47,9 @@ BuildRequires:  ocaml-re-devel
 BuildRequires:  ocaml-sexplib-devel
 BuildRequires:  ocaml-zarith-devel
 BuildRequires:  ocaml-zip-devel
-BuildRequires:  %{py3_dist sphinx}
-BuildRequires:  %{py3_dist sphinxcontrib-bibtex}
-BuildRequires:  tex(capt-of.sty)
-BuildRequires:  tex(comment.sty)
-BuildRequires:  tex(fncychap.sty)
-BuildRequires:  tex(framed.sty)
-BuildRequires:  tex(latex)
-BuildRequires:  tex(needspace.sty)
-BuildRequires:  tex(tabulary.sty)
-BuildRequires:  tex(tgtermes.sty)
-BuildRequires:  tex(upquote.sty)
-BuildRequires:  tex(wrapfig.sty)
-BuildRequires:  tex-urlbst
+BuildRequires:  rocq
+BuildRequires:  texlive-latex
+BuildRequires:  vim-filesystem

 Requires:       gtksourceview3%{?_isa}
 Requires:       hicolor-icon-theme
@ -82,26 +62,15 @@ Recommends:     flocq
 Provides:       bundled(js-jquery)

 # The corresponding Provides is not generated, so filter this out
-%global __requires_exclude ocaml\\\((Driver_ast|Why3)\\\)
-
-# This can be removed when F36 reaches EOL
-Obsoletes:      why < 2.41-12
-Provides:       why = 2.41-12%{?dist}
-Obsoletes:      why-jessie < 2.41-12
-Provides:       why-jessie = 2.41-12%{?dist}
-Obsoletes:      why-pvs-support < 2.41-12
-Provides:       why-pvs-support = 2.41-12%{?dist}
-
-# This can be removed when F39 reaches EOL
-Obsoletes:      %{name}-xemacs < 1.4.0-4
+%global __requires_exclude ocaml\\\(Driver_ast\\\)

 %description
-Why3 is the next generation of the Why software verification platform.
-Why3 clearly separates the purely logical specification part from
-generation of verification conditions for programs.  It features a rich
-library of proof task transformations that can be chained to produce a
-suitable input for a large set of theorem provers, including SMT
-solvers, TPTP provers, as well as interactive proof assistants.
+Why3 is the next generation of the Why software verification platform.  Why3
+clearly separates the purely logical specification part from generation of
+verification conditions for programs.  It features a rich library of proof
+task transformations that can be chained to produce a suitable input for a
+large set of theorem provers, including SMT solvers, TPTP provers, as well as
+interactive proof assistants.

 %package examples
 Summary:        Example inputs
@ -125,21 +94,17 @@ Summary:        Complete Why3 software verification platform suite
 Requires:       %{name}%{?_isa} = %{version}-%{release}
 Requires:       alt-ergo coq cvc5 E gappa yices-tools z3 zenon

-# This can be removed when F36 reaches EOL
-Obsoletes:      why-all < 2.41-12
-Provides:       why-all = 2.41-12%{?dist}
-
 %description all
-This package provides a complete software verification platform suite
-based on Why3, including various automated and interactive provers.
+This package provides a complete software verification platform suite based on
+Why3, including various automated and interactive provers.

 %package -n ocaml-%{name}
 Summary:        Software verification library for ocaml
 Requires:       ocaml-zip-devel%{?_isa}

 %description -n ocaml-%{name}
-This package contains an ocaml library that exposes the functionality
-of why3 to applications.
+This package contains an ocaml library that exposes the functionality of why3
+to applications.

 %package -n ocaml-%{name}-devel
 Summary:        Development files for using the ocaml-%{name} library
@ -151,8 +116,8 @@ Requires:       ocaml-sexplib-devel%{?_isa}
 Requires:       ocaml-zip-devel%{?_isa}

 %description -n ocaml-%{name}-devel
-This package contains development files needed to build applications
-that use the ocaml-%{name} library.
+This package contains development files needed to build applications that use
+the ocaml-%{name} library.

 %package proofgeneral
 Summary:        Why3 integration with ProofGeneral
@ -166,6 +131,7 @@ This package provides a why3 plugin for ProofGeneral.
 %prep
 %autosetup -p1

+%conf
 fixtimestamp() {
  touch -r $1.orig $1
  rm $1.orig
@ -174,9 +140,9 @@ fixtimestamp() {
 # Use the correct compiler flags, keep timestamps, and harden the build due to
 # network use.  Link the binaries with runtime compiled with -fPIC.
 # This avoids many link-time errors.
-sed -e "s|-Wall|%{build_cflags}|;s/ -O -g//" \
-    -e "s/cp /cp -p /" \
-    -e "s|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt \"%{build_ldflags}\"|" \
+sed -e 's|-Wall|%{build_cflags} %{build_ldflags}|;s/ -O -g//' \
+    -e 's/cp /cp -p /' \
+    -e 's|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt "%{build_ldflags}"|' \
    -i Makefile.in

 # Update the ProofGeneral integration instructions
@ -185,9 +151,11 @@ fixtimestamp share/whyitp/README

 %build
 %configure --enable-verbose-make --enable-bddinfer
+
 # FIXME: Parallel make sometimes fails
 make
-make doc
+# The documentation build is broken in the 1.8.0 release
+# make doc
 rm -f doc/html/.buildinfo examples/use_api/.merlin.in

 %install
@ -204,16 +172,16 @@ cd -
 %endif

 # Install the bash completion file
-mkdir -p %{buildroot}%{_datadir}/bash-completion/completions
-cp -p share/bash/%{name} %{buildroot}%{_datadir}/bash-completion/completions
+mkdir -p %{buildroot}%{bash_completions_dir}
+cp -p share/bash/%{name} %{buildroot}%{bash_completions_dir}

 # Install the zsh completion file
-mkdir -p %{buildroot}%{_datadir}/zsh/site-functions
-cp -p share/zsh/_why3 %{buildroot}%{_datadir}/zsh/site-functions
+mkdir -p %{buildroot}%{zsh_completions_dir}
+cp -p share/zsh/_why3 %{buildroot}%{zsh_completions_dir}

 # Install the LaTeX style
-mkdir -p %{buildroot}%{_texmf}/tex/latex/why3
-cp -p share/latex/why3lang.sty %{buildroot}%{_texmf}/tex/latex/why3
+mkdir -p %{buildroot}%{_texmf_main}/tex/latex/why3
+cp -p share/latex/why3lang.sty %{buildroot}%{_texmf_main}/tex/latex/why3

 # Move the gtksourceview language file to the right place
 mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0
@ -225,9 +193,9 @@ mkdir -p %{buildroot}%{_datadir}/applications
 desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE1}

 # Install the icon
-mkdir -p %{buildroot}%{_datadir}/icons/hicolor/scalable
+mkdir -p %{buildroot}%{_datadir}/icons/hicolor/scalable/apps
 cp -p share/images/src/logo-kim.svg \
-      %{buildroot}%{_datadir}/icons/hicolor/scalable/%{name}.svg
+      %{buildroot}%{_datadir}/icons/hicolor/scalable/apps/%{name}.svg

 # Install the AppStream metadata
 mkdir -p %{buildroot}%{_metainfodir}
@ -236,10 +204,10 @@ appstream-util validate-relax --nonet \
  %{buildroot}%{_metainfodir}/fr.lri.%{name}.metainfo.xml

 # Move the vim file to the right place
-mkdir -p %{buildroot}%{_datadir}/vim/vimfiles
+mkdir -p %{buildroot}%{vimfiles_root}
 mv %{buildroot}%{_datadir}/%{name}/vim/ftdetect \
   %{buildroot}%{_datadir}/%{name}/vim/syntax \
-   %{buildroot}%{_datadir}/vim/vimfiles
+   %{buildroot}%{vimfiles_root}

 # Byte compile the Emacs support files
 cp -p share/whyitp/whyitp.el %{buildroot}%{_emacs_sitelispdir}
@ -257,21 +225,22 @@ chmod 0755 %{buildroot}%{_bindir}/* \
           %{buildroot}%{ocamldir}/%{name}/*.cmxs

 %files
-%doc AUTHORS CHANGES.md README.md doc/html doc/latex/manual.pdf
+%doc AUTHORS CHANGES.md README.md
 %license LICENSE
 %{_bindir}/%{name}
 %{_bindir}/isabelle_client
+%{bash_completions_dir}/why3
+%{zsh_completions_dir}/_why3
 %{_datadir}/%{name}/
 %{_datadir}/applications/fr.lri.%{name}.desktop
-%{_datadir}/bash-completion/completions/why3
+%{_datadir}/gtksourceview-3.0/language-specs/coma.lang
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}.lang
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}c.lang
 %{_datadir}/gtksourceview-3.0/language-specs/%{name}py.lang
-%{_datadir}/icons/hicolor/scalable/%{name}.svg
-%{_datadir}/vim/vimfiles/ftdetect/%{name}.vim
-%{_datadir}/vim/vimfiles/syntax/%{name}.vim
-%{_datadir}/zsh/
-%{_texmf}/tex/latex/why3/
+%{_datadir}/icons/hicolor/scalable/apps/%{name}.svg
+%{vimfiles_root}/ftdetect/%{name}.vim
+%{vimfiles_root}/syntax/%{name}.vim
+%{_texmf_main}/tex/latex/why3/
 %{_libdir}/%{name}/
 %{_metainfodir}/fr.lri.%{name}.metainfo.xml

@ -308,481 +277,4 @@ chmod 0755 %{buildroot}%{_bindir}/* \
 %files all

 %changelog
-* Sat Sep  9 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-6
- Rebuild for ocaml-ocamlgraph 2.1.0
-
-* Sat Jul 29 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-5
- Require cvc5 instead of cvc4
-
-* Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-4
- Rebuild for ocaml-zarith 1.13
-
-* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 1.6.0-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
-
-* Tue Jul 18 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-2
- Validate metadata with appstream-util
-
-* Thu Jul 13 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-2
- Rebuild for mpfr 4.2.0
-
-* Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 1.6.0-1
- Version 1.6.0
- Enable inference with BDDs
- Add patch for coq 8.17 support
-
-* Sat Apr  1 2023 Jerry James <loganjerry@gmail.com> - 1.5.1-7
- Rebuild for coq 8.17.0
-
-* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 1.5.1-6
- Rebuild OCaml packages for F38
-
-* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 1.5.1-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
-
-* Fri Jan  6 2023 Jerry James <loganjerry@gmail.com> - 1.5.1-4
- BR tex(tgtermes.sty) to fix FTBFS with TeXLive 2022
-
-* Sat Nov 26 2022 Jerry James <loganjerry@gmail.com> - 1.5.1-3
- Rebuild for coq 8.16.1
-
-* Tue Nov  1 2022 Jerry James <loganjerry@gmail.com> - 1.5.1-2
- Rebuild for ocaml-ppxlib 0.28.0
-
-* Fri Sep 16 2022 Jerry James <loganjerry@gmail.com> - 1.5.1-1
- Version 1.5.1
-
-* Thu Aug 18 2022 Jerry James <loganjerry@gmail.com> - 1.5.0-3
- Rebuild to fix coq dependency
- Convert License tag to SPDX
-
-* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 1.5.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
-
-* Tue Jul 19 2022 Jerry James <loganjerry@gmail.com> - 1.5.0-1
- Remove i686 support
-
-* Thu Jul  7 2022 Jerry James <loganjerry@gmail.com> - 1.5.0-1
- Version 1.5.0
- Add ocaml-mlmpfr support
- Drop unmaintained man pages
- Use new OCaml macros
-
-* Sun Jun 19 2022 Richard W.M. Jones <rjones@redhat.com> - 1.4.1-3
- OCaml 4.14.0 rebuild
-
-* Fri Mar 25 2022 Jerry James <loganjerry@gmail.com> - 1.4.1-2
- Rebuild for coq 8.15.1
-
-* Mon Feb 28 2022 Jerry James <loganjerry@gmail.com> - 1.4.1-1
- Version 1.4.1
-
-* Fri Feb 04 2022 Richard W.M. Jones <rjones@redhat.com> - 1.4.0-11
- OCaml 4.13.1 rebuild to remove package notes
-
-* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 1.4.0-10
- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
-
-* Mon Jan 17 2022 Jerry James <loganjerry@gmail.com> - 1.4.0-9
- Rebuild for menhir 20211230
-
-* Mon Dec 27 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-8
- Rebuild for alt-ergo 2.3.0 and ocaml-zip 1.11
-
-* Tue Nov 30 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-7
- Rebuild for coq 8.14.1, sexplib0 0.15.0 and menhir 20211128
-
-* Thu Oct 21 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-6
- Rebuild for coq 8.14.0 and menhir 20211012
- Add -coq8.14 patch
- Drop XEmacs support
-
-* Tue Oct 05 2021 Richard W.M. Jones <rjones@redhat.com> - 1.4.0-5
- OCaml 4.13.1 build
-
-* Mon Oct 04 2021 Richard W.M. Jones <rjones@redhat.com> - 1.4.0-4
- Try to build on s390x with OCaml 4.13
-
-* Fri Jul 30 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-3
- Rebuild for rebuilt coq
-
-* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 1.4.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
-
-* Wed Jul 14 2021 Jerry James <loganjerry@gmail.com> - 1.4.0-1
- Version 1.4.0
- Drop all patches
- Validate with appstreamcli instead of appstream-util
-
-* Tue Jun  8 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-9
- Rebuild for ocaml-menhir 20210419
-
-* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-8
- Rebuild for coq 8.13.1 and ocaml-zarith 1.12
-
-* Tue Mar  2 11:18:12 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 1.3.3-7
- OCaml 4.12.0 build
-
-* Sat Feb 20 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-6
- Rebuild for coq 8.13.0
- Update metainfo and install in metainfodir
-
-* Wed Jan 27 2021 Fedora Release Engineering <releng@fedoraproject.org> - 1.3.3-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
-
-* Sat Jan  2 2021 Jerry James <loganjerry@gmail.com> - 1.3.3-4
- Rebuild for flocq 3.4.0
-
-* Wed Dec 23 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-3
- Rebuild for coq 8.12.2
-
-* Wed Dec  2 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-2
- Rebuild for coq 8.12.1 and menhir 20201201
-
-* Fri Sep 25 2020 Jerry James <loganjerry@gmail.com> - 1.3.3-1
- Version 1.3.3
-
-* Wed Sep 02 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-14
- OCaml 4.11.1 rebuild
-
-* Tue Sep  1 2020  Jerry James <loganjerry@gmail.com> - 1.3.1-13
- Rebuild for coq 8.12.0
-
-* Mon Aug 24 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-13
- OCaml 4.11.0 rebuild
-
-* Thu Aug  6 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-12
- Rebuild for ocaml-lablgtk3 3.1.1 and ocaml-menhir 20200624
-
-* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 1.3.1-11
- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
-
-* Mon Jun 15 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-10
- Rebuild for coq 8.11.2
-
-* Sat Jun 13 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-9
- Rebuild for flocq 3.3.1
- Build the coq files with the native compiler when possible
-
-* Wed May 20 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-8
- Rebuild for coq 8.11.1
-
-* Tue May 05 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-7
- OCaml 4.11.0+dev2-2020-04-22 rebuild
-
-* Sun Apr 12 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-6
- Make the dependencies on ocaml-num and ocaml-zip explicit (bz 1795083)
-
-* Wed Apr  8 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-5
- Rebuild for flocq 3.2.1
-
-* Sun Apr 05 2020 Richard W.M. Jones <rjones@redhat.com> - 1.3.1-4
- Update all OCaml dependencies for RPM 4.16.
-
-* Wed Apr  1 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-3
- Do not build with mlmpfr; symbols clash with mlgmpidl, causing frama-c to
-  fail to start
- Obsolete the why2 packages
-
-* Sat Mar 28 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-2
- Remove useless BRs and Rs (bz 1817878)
-
-* Wed Mar 25 2020 Jerry James <loganjerry@gmail.com> - 1.3.1-1
- Version 1.3.1
-
-* Fri Jan 31 2020 Fedora Release Engineering <releng@fedoraproject.org> - 1.2.1-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
-
-* Wed Jan 22 2020 Jerry James <loganjerry@gmail.com> - 1.2.1-3
- OCaml 4.10.0+beta1 rebuild.
-
-* Fri Dec 06 2019 Richard W.M. Jones <rjones@redhat.com> - 1.2.1-2
- OCaml 4.09.0 (final) rebuild.
-
-* Tue Oct 29 2019 Jerry James <loganjerry@gmail.com> - 1.2.1-1
- New upstream release
- Add -proofgeneral subpackage
- Add desktop and AppData files
-
-* Fri Oct 11 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-6
- Rebuild for ocaml-menhir 20190924
-
-* Fri Sep  6 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-5
- Rebuild for ocaml-zarith 1.9
-
-* Thu Aug  1 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-4
- Also install the library, for consumption by frama-c
-
-* Thu Aug  1 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-3
- Rebuild for flocq 3.2.0
-
-* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.2.0-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
-
-* Wed Jun  5 2019 Jerry James <loganjerry@gmail.com> - 1.2.0-1
- New upstream release
-
-* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 1.1.1-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
-
-* Sat Jan 26 2019 Jerry James <loganjerry@gmail.com> - 1.1.1-1
- New upstream release
-
-* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.88.3-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
-
-* Thu Jul 12 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-4
- OCaml 4.07.0 (final) rebuild.
-
-* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-3
- Bump release and rebuild.
-
-* Wed Jun 20 2018 Richard W.M. Jones <rjones@redhat.com> - 0.88.3-2
- OCaml 4.07.0-rc1 rebuild.
-
-* Mon Feb 12 2018 Jerry James <loganjerry@gmail.com> - 0.88.3-1
- New upstream release
-
-* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.88.2-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
-
-* Sat Dec  9 2017 Jerry James <loganjerry@gmail.com> - 0.88.2-1
- New upstream release
-
-* Fri Nov 17 2017 Richard W.M. Jones <rjones@redhat.com> - 0.88.1-1
- New upstream version 0.88.1.
- OCaml 4.06.0 rebuild.
-
-* Sat Oct  7 2017 Jerry James <loganjerry@gmail.com> - 0.88.0-1
- New usptream release
-
-* Thu Oct  5 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-12
- Rebuild for flocq 2.6.0
-
-* Wed Sep 06 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-11
- OCaml 4.05.0 rebuild.
-
-* Thu Aug 03 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-10
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Binutils_Mass_Rebuild
-
-* Thu Jul 27 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-9
- Rebuilt for https://fedoraproject.org/wiki/Fedora_27_Mass_Rebuild
-
-* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-8
- Bump release and rebuild.
-
-* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-7
- Bump release and rebuild.
-
-* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-6
- Bump release and rebuild.
-
-* Tue Jun 27 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-5
- OCaml 4.04.2 rebuild.
-
-* Fri May 12 2017 Richard W.M. Jones <rjones@redhat.com> - 0.87.3-4
- OCaml 4.04.1 rebuild.
-
-* Fri Mar 24 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-3
- Rebuild to fix coq consistency issue
-
-* Sat Feb 11 2017 Fedora Release Engineering <releng@fedoraproject.org> - 0.87.3-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_26_Mass_Rebuild
-
-* Thu Jan 12 2017 Jerry James <loganjerry@gmail.com> - 0.87.3-1
- New upstream release
-
-* Mon Nov 07 2016 Richard W.M. Jones <rjones@redhat.com> - 0.87.2-4
- Rebuild for OCaml 4.04.0.
-
-* Fri Oct 28 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-3
- Rebuild for coq 8.5pl3
- Remove obsolete scriptlets
- Fix install location of why3lang.sty
-
-* Thu Sep 29 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-2
- Rebuild for flocq 2.5.2 and gappalib-coq 1.3.1
-
-* Fri Sep  2 2016 Jerry James <loganjerry@gmail.com> - 0.87.2-1
- New upstream release
-
-* Wed Jul 13 2016 Jerry James <loganjerry@gmail.com> - 0.87.1-2
- Rebuild for coq 8.5pl2
-
-* Wed Jun  1 2016 Jerry James <loganjerry@gmail.com> - 0.87.1-1
- New upstream release
-
-* Fri Apr 22 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-3
- Rebuild for coq 8.5pl1
-
-* Sat Apr 16 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-2
- Rebuild for ocaml-ocamlgraph 1.8.7
-
-* Fri Mar 18 2016 Jerry James <loganjerry@gmail.com> - 0.87.0-1
- New upstream release
- Drop boomy icon removal; upstream no longer ships them
-
-* Fri Feb 12 2016 Jerry James <loganjerry@gmail.com> - 0.86.3-1
- New upstream release
- Use camlp4 in preference to camlp5
-
-* Fri Feb 05 2016 Fedora Release Engineering <releng@fedoraproject.org> - 0.86.2-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
-
-* Wed Nov 25 2015 Jerry James <loganjerry@gmail.com> - 0.86.2-2
- Rebuild for ocaml-zarith 1.4.1 and ocaml-menhir 20151112
-
-* Wed Oct 14 2015 Jerry James <loganjerry@gmail.com> - 0.86.2-1
- New upstream release
- Do not ship the nonfree boomy icons
-
-* Wed Jun 24 2015 Richard W.M. Jones <rjones@redhat.com> - 0.86.1-2
- ocaml-4.02.2 final rebuild.
-
-* Mon Jun 22 2015 Jerry James <loganjerry@gmail.com> - 0.86.1-1
- New upstream release
-
-* Wed Jun 17 2015 Richard W.M. Jones <rjones@redhat.com> - 0.86-2
- ocaml-4.02.2 rebuild.
-
-* Sat May 16 2015 Jerry James <loganjerry@gmail.com> - 0.86-1
- New upstream release
-
-* Sat Apr 11 2015 Jerry James <loganjerry@gmail.com> - 0.85-9
- Rebuild for coq 8.4pl6
-
-* Wed Mar 18 2015 Jerry James <loganjerry@gmail.com> - 0.85-8
- Rebuild for ocaml-ocamlgraph 1.8.6
-
-* Sat Feb 21 2015 Jerry James <loganjerry@gmail.com> - 0.85-7
- Note bundled jquery
- Fix sed expression separators for new RPM_OPT_FLAGS and RPM_LD_FLAGS
-
-* Wed Feb 18 2015 Richard W.M. Jones <rjones@redhat.com> - 0.85-6
- ocaml-4.02.1 rebuild.
-
-* Thu Nov  6 2014 Jerry James <loganjerry@gmail.com> - 0.85-5
- Rebuild for ocaml-camlp5 6.12
-
-* Thu Oct 30 2014 Jerry James <loganjerry@gmail.com> - 0.85-4
- Rebuild for coq 8.4pl5
-
-* Tue Oct 14 2014 Jerry James <loganjerry@gmail.com> - 0.85-3
- Rebuild for ocaml-zarith 1.3
-
-* Thu Sep 18 2014 Jerry James <loganjerry@gmail.com> - 0.85-2
- Bump and rebuild
-
-* Wed Sep 17 2014 Jerry James <loganjerry@gmail.com> - 0.85-1
- New upstream release
- New source URL
-
-* Tue Sep  2 2014 Jerry James <loganjerry@gmail.com> - 0.84-1
- New upstream release
- Fix license handling
-
-* Mon Aug 25 2014 Jerry James <loganjerry@gmail.com> - 0.83-14
- Rebuild for new gappalib-coq build
-
-* Sun Aug 24 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-13
- ocaml-4.02.0+rc1 rebuild.
-
-* Mon Aug 18 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.83-12
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
-
-* Mon Aug  4 2014 Jerry James <loganjerry@gmail.com> - 0.83-11
- Rebuild for new gappalib-coq build
-
-* Sat Aug 02 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-10
- ocaml-4.02.0-0.8.git10e45753.fc22 rebuild.
-
-* Fri Aug 01 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-9
- OCaml 4.02.0 beta rebuild.
-
-* Thu Jun 26 2014 Jerry James <loganjerry@gmail.com> - 0.83-8
- Linking with -z relro -z now breaks plugins; omit "-z now"
-
-* Sun Jun 08 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.83-7
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
-
-* Tue May 13 2014 Jerry James <loganjerry@gmail.com> - 0.83-6
- Rebuild for coq 8.4pl4
-
-* Mon Apr 21 2014 Jerry James <loganjerry@gmail.com> - 0.83-5
- Rebuild for flocq 2.3.0 and ocamlgraph 1.8.5
- Drop unnecessary sqlite-devel BR
-
-* Tue Apr 15 2014 Richard W.M. Jones <rjones@redhat.com> - 0.83-4
- Remove ocaml_arches macro (RHBZ#1087794).
-
-* Mon Mar 24 2014 Jerry James <loganjerry@gmail.com> - 0.83-3
- Apply upstream fix for building with ocaml-zarith
- Fix file encodings
- Fix permission bits
-
-* Tue Mar 18 2014 Jerry James <loganjerry@gmail.com> - 0.83-2
- Back out the post-release fix to the Coq printer, which breaks Frama-C
-
-* Fri Mar 14 2014 Jerry James <loganjerry@gmail.com> - 0.83-1
- New upstream release
- Use cvc4 instead of cvc3
-
-* Wed Feb 26 2014 Jerry James <loganjerry@gmail.com> - 0.82-2
- Rebuild for ocamlgraph 1.8.4
- BR ocaml-findlib instead of ocaml-findlib-devel
-
-* Fri Dec 13 2013 Jerry James <loganjerry@gmail.com> - 0.82-1
- New upstream release
- Drop upstreamed patches
- Add -examples subpackage
- Install LaTeX style
- Turn off frama-c support at upstream's request
-
-* Mon Sep 30 2013 Jerry James <loganjerry@gmail.com> - 0.81-6
- Apply upstream fix for change in the alt-ergo timelimit option
-
-* Tue Sep 17 2013 Jerry James <loganjerry@gmail.com> - 0.81-5
- Rebuild for OCaml 4.01.0
- Enable debuginfo for the ocaml sources
-
-* Sun Aug 04 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.81-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
-
-* Fri Jun 21 2013 Jerry James <loganjerry@gmail.com> - 0.81-3
- Rebuild for frama-c Fluorine 20130601
-
-* Thu May 23 2013 Jerry James <loganjerry@gmail.com> - 0.81-2
- Rebuild for frama-c Fluorine 20130501
-
-* Fri May 10 2013 Jerry James <loganjerry@gmail.com> - 0.81-1
- New upstream release
- Disable PVS support for now; it requires the NASA libraries
- Fix the conflict between the why and why3 Emacs packages (bz 913522)
- Disable parallel builds due to intermittent build failures
-
-* Fri Feb 15 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.73-5
- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
-
-* Mon Jan  7 2013 Jerry James <loganjerry@gmail.com> - 0.73-4
- Rebuild for coq 8.4pl1
-
-* Fri Dec 14 2012 Richard W.M. Jones <rjones@redhat.com> - 0.73-3
- Rebuild for OCaml 4.00.1.
-
-* Thu Aug 23 2012 Jerry James <loganjerry@gmail.com> - 0.73-2
- Rebuild for coq 8.4
-
-* Thu Aug  2 2012 Jerry James <loganjerry@gmail.com> - 0.73-1
- New upstream release
-
-* Sun Jul 22 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 0.71-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
-
-* Thu Apr 19 2012 Jerry James <loganjerry@gmail.com> - 0.71-2
- Add missing sqlite-devel BR
- Do not move the coq plugin
- Generate debuginfo for the sole C program
- Add man pages
-
-* Fri Dec 16 2011 Jerry James <loganjerry@gmail.com> - 0.71-1
- Initial RPM
+%autochangelog
Author	SHA1	Message	Date
Jerry James	cb0c5c7d69	Rebuild for ocaml-ppx-deriving 6.1.3	2026-07-29 12:32:20 -06:00
Fedora Release Engineering	679e804de1	Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild	2026-07-17 08:48:20 +00:00
Jerry James	f8b7cae4a6	OCaml 5.5.0 rebuild	2026-07-09 20:52:51 -06:00
Jerry James	cfd29ec6fd	Rebuild for rocq 9.2.0	2026-04-16 12:23:41 -06:00
Jerry James	f6d80e1a29	Rebuild for rocq 9.1.1 - Add patch to avoid Zmod, removed in rocq 9.1	2026-03-19 21:38:47 -06:00
Richard W.M. Jones	1889b3d497	OCaml 5.4.1 rebuild	2026-02-21 00:12:57 +00:00
Jerry James	5a8173d697	Rebuild for ocaml-menhir-20260209	2026-02-11 20:03:06 -07:00
Jerry James	e7d64b7f0f	Rebuild for ocaml-menhir 20260203	2026-02-06 17:00:40 -07:00
Jerry James	a4c3815695	Rebuild for ocaml-menhir 20260122	2026-02-02 16:26:22 -07:00
Fedora Release Engineering	d3d801816f	Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild	2026-01-17 20:13:59 +00:00
Jerry James	e51d1ba9fc	Reflow the description text	2026-01-14 08:53:03 -07:00
Richard W.M. Jones	c7de9116b8	OCaml 5.4.0 rebuild	2025-10-14 20:54:37 +01:00
Jerry James	10869d3c2e	Version 1.8.2	2025-09-16 15:25:39 -06:00
Jerry James	5d0415f73c	Rebuild for ocaml-menhir 20250903	2025-09-05 11:14:24 -06:00
Jerry James	dfde276402	Rebuild for ocaml-unionfind 20250818	2025-08-22 10:25:54 -06:00
Jerry James	f24429dc72	BR vim-filesystem for %{vimfiles_root}	2025-08-10 11:47:45 -06:00
Jerry James	32bd519ce7	Use %{vimfiles_root}	2025-08-10 11:23:17 -06:00
Jerry James	25a38102cf	Bump and rebuild	2025-08-10 11:02:02 -06:00
Fedora Release Engineering	ddf170d66a	Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild	2025-07-25 20:24:57 +00:00
Jerry James	eef9515e6d	Rebuild to fix OCaml dependencies	2025-07-12 16:48:04 -06:00
Jerry James	92927d0b7d	Version 1.8.1 - All patches have been upstreamed	2025-06-09 15:05:43 -06:00
Jerry James	9ec4d214c6	Rebuild for bumped ocaml-mlgmpidl	2025-06-07 10:34:13 -06:00
Jerry James	525daf1052	Rebuild for ocaml-ocamlgraph 2.2.0	2025-04-15 14:09:32 -06:00
Jerry James	d9a95c6189	Rebuild for flocq 4.2.1	2025-02-13 14:41:57 -07:00
Jerry James	7ab80d8d3e	Add patch for C23 compatibility	2025-01-22 16:01:25 -07:00
Fedora Release Engineering	3d1348dd56	Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild	2025-01-19 15:00:39 +00:00
Jerry James	d46d748db4	OCaml 5.3.0 rebuild for Fedora 42 - Version 1.8.0 - Disable documentation build due to bugs in 1.8.0	2025-01-10 10:30:03 -07:00
Jerry James	98156958f8	Convert to %autorelease and %autochangelog [skip changelog]	2025-01-10 10:28:18 -07:00
Jerry James	88b9f2e9c7	Fix the location of the icon	2024-10-14 15:14:21 -06:00
Jerry James	b798c9103b	Rebuild for ocaml-re 1.13.3	2024-10-06 15:16:41 -06:00
Jerry James	acda593bf2	Rebuild for ocaml-menhir 20240715, ocaml-ppxlib 0.33.0, and ocaml-zip 1.1.2	2024-08-05 11:24:06 -06:00
Fedora Release Engineering	2daac66f57	Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild	2024-07-20 09:20:04 +00:00
Jerry James	664bbc3564	Rebuild for ocaml-zarith 1.14	2024-07-16 11:13:09 -06:00
Jerry James	b4ad7f2eed	Rebuild for ocaml-ppx-sexp-conv 0.17.0	2024-07-03 16:58:56 -06:00
Richard W.M. Jones	c6f7681992	OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix OCaml 5.2.0 ppc64le fix	2024-06-19 19:28:35 +01:00
Jerry James	356eda9812	Rebuild for apron 0.9.15 - New upstream URL	2024-06-13 14:38:24 -06:00
Richard W.M. Jones	0aeedb81c5	OCaml 5.2.0 for Fedora 41	2024-05-30 10:30:35 +01:00
Jerry James	8000f2ad4a	Version 1.7.2	2024-04-18 09:47:00 -06:00
Richard W.M. Jones	44636b4555	Use %{bash_completions_dir} macro	2024-03-25 11:27:20 +00:00
Jerry James	84cb61b8ea	Build again because koji ran out of disk space	2024-02-02 18:44:17 -07:00
Jerry James	8d5ff06bc5	Version 1.7.1	2024-02-02 16:41:48 -07:00
Fedora Release Engineering	12c78c7f05	Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild	2024-01-27 08:45:59 +00:00
Jerry James	e86bfd3112	Version 1.7.0. Drop upstreamed coq patch.	2024-01-02 12:34:03 -07:00
Richard W.M. Jones	8d82ad63f7	OCaml 5.1.1 + s390x code gen fix for Fedora 40	2023-12-18 19:26:12 +00:00
Richard W.M. Jones	8b5401104d	OCaml 5.1.1 rebuild for Fedora 40	2023-12-12 19:17:54 +00:00
Richard W.M. Jones	b3fca63993	OCaml 5.1 rebuild for Fedora 40	2023-10-05 21:46:07 +01:00
Jerry James	c96ac3b16a	Remove old obsoletes	2023-10-04 23:18:14 -06:00