Rebuild to fix rocq dependencies

- Add patch to avoid deprecated usage

README.md

@@ -0,0 +1,9 @@
+# zenon
+
+Zenon is an extensible authomated theorem prover whose main claim to fame is
+that it produces actual proofs of theorems.  Correctness is an explicit
+non-goal in the design of Zenon: the proof output needs to be checked by
+another program before the theorem is considered proved.  As a consequence,
+Zenon is not designed for direct use by humans, but rather for interfacing
+into formal proof systems, such as interactive proof assistants and
+non-interactive proof checkers.

sources

@@ -1,2 +1,2 @@
-SHA512 (zenon-0.8.4.tar.gz) = a60ad321e7eedc00390d11ff91f25d64c7a3fe2eafa23a330e345df02a30ca6964a40e4495b7eeb25e19ed9b7f61b65772c3184ff2b2f85b03e63dc481645e91
+SHA512 (zenon-0.8.5.tar.gz) = dc97cc02bcc2e76a1130f4f7e44ba9839126b5e15f4488ac32d47aef330cbb9ea8c2f1b34f8543ed243587e95848a7187c003a300feed0da64ec81f4501b3bdb
 SHA512 (zenlpar07.pdf) = f8a24ba1c32015ea315946042b39f0b629094553097f43c8fb37041450d39b64e3a781006bdcbae42919104907efec9f0cf065d675f3ff09af891d9d28c2549f

zenon-coq89.patch

@@ -1,174 +0,0 @@
---- zenon_coqbool.v.orig	2018-09-18 09:01:37.000000000 -0600
-+++ zenon_coqbool.v	2019-05-31 09:34:36.433667055 -0600
-@@ -143,7 +143,7 @@ Proof.
-   intros A B r cond; unfold Is_true; destruct cond; auto.
- Qed.
- 
--Implicit Arguments zenon_coqbool_ite_rel_l [A B].
-+Arguments zenon_coqbool_ite_rel_l [A B].
- 
- Lemma zenon_coqbool_ite_rel_r :
-   forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B),
-@@ -154,7 +154,7 @@ Proof.
-   intros A B r e1 cond; unfold Is_true; destruct cond; auto.
- Qed.
- 
--Implicit Arguments zenon_coqbool_ite_rel_r [A B].
-+Arguments zenon_coqbool_ite_rel_r [A B].
- 
- Lemma zenon_coqbool_ite_rel_nl :
-   forall (A B : Type) (r: A -> B -> Prop) (cond : bool) (thn els : A) (e2 : B),
-@@ -165,7 +165,7 @@ Proof.
-   intros A B r cond; unfold Is_true; destruct cond; auto.
- Qed.
- 
--Implicit Arguments zenon_coqbool_ite_rel_nl [A B].
-+Arguments zenon_coqbool_ite_rel_nl [A B].
- 
- Lemma zenon_coqbool_ite_rel_nr :
-   forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B),
-@@ -176,7 +176,7 @@ Proof.
-   intros A B r e1 cond; unfold Is_true; destruct cond; auto.
- Qed.
- 
--Implicit Arguments zenon_coqbool_ite_rel_nr [A B].
-+Arguments zenon_coqbool_ite_rel_nr [A B].
- 
- (* ************************************************ *)
- 
-@@ -216,19 +216,19 @@ Definition zenon_coqbool_ite_rel_l_s :=
-   fun A B r i t e e2 c h1 h2
-   => @zenon_coqbool_ite_rel_l A B r i t e e2 h1 h2 c
- .
--Implicit Arguments zenon_coqbool_ite_rel_l_s [A B].
-+Arguments zenon_coqbool_ite_rel_l_s [A B].
- Definition zenon_coqbool_ite_rel_r_s :=
-   fun A B r e1 i t e c h1 h2
-   => @zenon_coqbool_ite_rel_r A B r e1 i t e h1 h2 c
- .
--Implicit Arguments zenon_coqbool_ite_rel_r_s [A B].
-+Arguments zenon_coqbool_ite_rel_r_s [A B].
- Definition zenon_coqbool_ite_rel_nl_s :=
-   fun A B r i t e e2 c h1 h2
-   => @zenon_coqbool_ite_rel_nl A B r i t e e2 h1 h2 c
- .
--Implicit Arguments zenon_coqbool_ite_rel_nl_s [A B].
-+Arguments zenon_coqbool_ite_rel_nl_s [A B].
- Definition zenon_coqbool_ite_rel_nr_s :=
-   fun A B r e1 i t e c h1 h2
-   => @zenon_coqbool_ite_rel_nr A B r e1 i t e h1 h2 c
- .
--Implicit Arguments zenon_coqbool_ite_rel_nr_s [A B].
-+Arguments zenon_coqbool_ite_rel_nr_s [A B].
---- zenon_focal.v.orig	2018-09-18 09:01:37.000000000 -0600
-+++ zenon_focal.v	2019-05-31 09:34:54.814494601 -0600
-@@ -198,7 +198,7 @@ Proof.
-   intros A B r cond; unfold Is_true; destruct cond; auto.
- Qed.
- 
--Implicit Arguments zenon_focal_ite_rel_l [A B].
-+Arguments zenon_focal_ite_rel_l [A B].
- 
- Lemma zenon_focal_ite_rel_r :
-   forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B),
-@@ -209,7 +209,7 @@ Proof.
-   intros A B r e1 cond; unfold Is_true; destruct cond; auto.
- Qed.
- 
--Implicit Arguments zenon_focal_ite_rel_r [A B].
-+Arguments zenon_focal_ite_rel_r [A B].
- 
- Lemma zenon_focal_ite_rel_nl :
-   forall (A B : Type) (r: A -> B -> Prop) (cond : bool) (thn els : A) (e2 : B),
-@@ -220,7 +220,7 @@ Proof.
-   intros A B r cond; unfold Is_true; destruct cond; auto.
- Qed.
- 
--Implicit Arguments zenon_focal_ite_rel_nl [A B].
-+Arguments zenon_focal_ite_rel_nl [A B].
- 
- Lemma zenon_focal_ite_rel_nr :
-   forall (A B : Type) (r: A -> B -> Prop) (e1 : A) (cond : bool) (thn els : B),
-@@ -231,7 +231,7 @@ Proof.
-   intros A B r e1 cond; unfold Is_true; destruct cond; auto.
- Qed.
- 
--Implicit Arguments zenon_focal_ite_rel_nr [A B].
-+Arguments zenon_focal_ite_rel_nr [A B].
- 
- Lemma zenon_focal_istrue_true : forall e,
-   (e = true -> False) -> (Is_true e -> False).
-@@ -313,19 +313,19 @@ Definition zenon_focal_ite_rel_l_s :=
-   fun A B r i t e e2 c h1 h2
-   => @zenon_focal_ite_rel_l A B r i t e e2 h1 h2 c
- .
--Implicit Arguments zenon_focal_ite_rel_l_s [A B].
-+Arguments zenon_focal_ite_rel_l_s [A B].
- Definition zenon_focal_ite_rel_r_s :=
-   fun A B r e1 i t e c h1 h2
-   => @zenon_focal_ite_rel_r A B r e1 i t e h1 h2 c
- .
--Implicit Arguments zenon_focal_ite_rel_r_s [A B].
-+Arguments zenon_focal_ite_rel_r_s [A B].
- Definition zenon_focal_ite_rel_nl_s :=
-   fun A B r i t e e2 c h1 h2
-   => @zenon_focal_ite_rel_nl A B r i t e e2 h1 h2 c
- .
--Implicit Arguments zenon_focal_ite_rel_nl_s [A B].
-+Arguments zenon_focal_ite_rel_nl_s [A B].
- Definition zenon_focal_ite_rel_nr_s :=
-   fun A B r e1 i t e c h1 h2
-   => @zenon_focal_ite_rel_nr A B r e1 i t e h1 h2 c
- .
--Implicit Arguments zenon_focal_ite_rel_nr_s [A B].
-+Arguments zenon_focal_ite_rel_nr_s [A B].
---- zenon_induct.v.orig	2018-09-18 09:01:37.000000000 -0600
-+++ zenon_induct.v	2019-05-31 09:39:07.572218768 -0600
-@@ -12,13 +12,13 @@ Lemma zenon_induct_f_equal : forall (T1
-   (f x = f y -> False) -> (x = y -> False).
-   Proof. intros T1 T2 x y f H1 H2. apply H1. subst x. auto. Qed.
- 
--Implicit Arguments zenon_induct_f_equal [T1 T2].
-+Arguments zenon_induct_f_equal [T1 T2].
- 
- Definition zenon_induct_f_equal_s :=
-   fun t1 t2 x y f c h => @zenon_induct_f_equal t1 t2 x y f h c
- .
- 
--Implicit Arguments zenon_induct_f_equal_s [t1 t2].
-+Arguments zenon_induct_f_equal_s [t1 t2].
- 
- Lemma zenon_induct_case_subs : forall (T : Type) (b a : T) P,
-   (b = a -> P(a) -> False) -> b = a -> P(b) -> False.
---- zenon.v.orig	2018-09-18 09:01:37.000000000 -0600
-+++ zenon.v	2019-05-31 09:34:15.884859849 -0600
-@@ -71,7 +71,7 @@ Lemma zenon_notallex : forall (T : Type)
- Proof.
-   firstorder. apply H0. intro x. apply NNPP. intro nPx. apply (H x nPx).
- Qed.
--Implicit Arguments zenon_notallex [T].
-+Arguments zenon_notallex [T].
- 
- Lemma zenon_subst :
-   forall (T : Type) (P : T -> Prop) (a b : T),
-@@ -111,7 +111,7 @@ Definition zenon_notequiv_s := fun P Q c
- Definition zenon_ex_s := fun T P c h => zenon_ex T P h c.
- Definition zenon_notall_s := fun T P c h => zenon_notall T P h c.
- Definition zenon_notallex_s := fun T P c h => @zenon_notallex T P h c.
--Implicit Arguments zenon_notallex_s [T].
-+Arguments zenon_notallex_s [T].
- 
- Definition zenon_subst_s := fun T P x y c h i => zenon_subst T P x y h i c.
- Definition zenon_pnotp_s := fun P Q c h i => zenon_pnotp P Q h i c.
-@@ -142,9 +142,9 @@ Proof.
-   auto.
- Qed.
- 
--Implicit Arguments zenon_recfun_unfold [A].
-+Arguments zenon_recfun_unfold [A].
- 
- Definition zenon_recfun_unfold_s :=
-   fun A P a b eqn c h => @zenon_recfun_unfold A P a b eqn h c
- .
--Implicit Arguments zenon_recfun_unfold_s [A].
-+Arguments zenon_recfun_unfold_s [A].

zenon-deprecated.patch

@@ -0,0 +1,34 @@
+--- zenon-0.8.5/zenon_coqbool.v.orig	2020-10-23 09:19:07.000000000 -0600
++++ zenon-0.8.5/zenon_coqbool.v	2026-03-03 16:33:33.636474063 -0700
+@@ -1,6 +1,6 @@
+ (*  Copyright 2004 INRIA  *)
+ 
+-Require Export Bool.
++From Stdlib Require Export Bool.
+ 
+ Definition __g_not_b := negb.
+ Definition __g_and_b := andb.
+--- zenon-0.8.5/zenon_focal.v.orig	2020-10-23 09:19:07.000000000 -0600
++++ zenon-0.8.5/zenon_focal.v	2026-03-03 16:34:30.531982864 -0700
+@@ -1,8 +1,8 @@
+ (*  Copyright 2004 INRIA  *)
+ 
+-Require Export Bool.
+-Require Import ClassicalEpsilon.
+-Require List.
++From Stdlib Require Export Bool.
++From Stdlib Require Import ClassicalEpsilon.
++From Stdlib Require List.
+ 
+ (* magic: this whole file depends on the following definitions:
+    basics.and_b := andb
+--- zenon-0.8.5/zenon.v.orig	2020-10-23 09:19:07.000000000 -0600
++++ zenon-0.8.5/zenon.v	2026-03-03 16:33:06.988515450 -0700
+@@ -1,6 +1,6 @@
+ (*  Copyright 2004 INRIA  *)
+ 
+-Require Export Classical.
++From Stdlib Require Export Classical.
+ 
+ Lemma zenon_notnot : forall P : Prop,
+   P -> (~ P -> False).

zenon-ocaml.patch

@@ -1,55 +0,0 @@
---- coqterm.ml.orig	2018-09-18 09:01:37.000000000 -0600
-+++ coqterm.ml	2020-08-20 13:02:03.239490105 -0600
-@@ -447,7 +447,7 @@ let rec rm_lambdas l term =
-   | _, _ -> assert false
- ;;
- 
--let compare_hyps (name1, _) (name2, _) = Pervasives.compare name1 name2;;
-+let compare_hyps (name1, _) (name2, _) = Stdlib.compare name1 name2;;
- 
- let make_lemma { name = name; params = params; proof = proof } =
-   let f (ty, e) =
---- expr.ml.orig	2018-09-18 09:01:37.000000000 -0600
-+++ expr.ml	2020-08-20 13:01:38.415478986 -0600
-@@ -364,7 +364,7 @@ let hash = get_hash;;
- let equal = (==);;
- let compare x y =
-   match compare (hash x) (hash y) with
--  | 0 -> if equal x y then 0 else Pervasives.compare x y
-+  | 0 -> if equal x y then 0 else Stdlib.compare x y
-   | x when x < 0 -> -1
-   | _ -> 1
- ;;
---- ext_induct.ml.orig	2018-09-18 09:01:37.000000000 -0600
-+++ ext_induct.ml	2020-08-20 13:03:10.847520391 -0600
-@@ -96,8 +96,8 @@ let rec make_case accu e =
- 
- let compare_cases (cs1, _, _) (cs2, _, _) =
-   try
--    Pervasives.compare (Hashtbl.find constructor_table cs1).cd_num
--                       (Hashtbl.find constructor_table cs2).cd_num
-+    Stdlib.compare (Hashtbl.find constructor_table cs1).cd_num
-+                   (Hashtbl.find constructor_table cs2).cd_num
-   with Not_found -> raise Empty
- ;;
- 
---- lltoisar.ml.orig	2018-09-18 09:01:37.000000000 -0600
-+++ lltoisar.ml	2020-08-20 13:02:41.168507098 -0600
-@@ -21,7 +21,7 @@ let dict_empty = Dict.empty;;
- 
- module Int = struct
-   type t = int;;
--  let compare = Pervasives.compare;;
-+  let compare = Stdlib.compare;;
- end;;
- module Hypdict = Map.Make (Int);;
- 
-@@ -973,7 +973,7 @@ let rec get_nary_rules accu prf =
- let add_nary_rules oc lemmas =
-   let f lem = get_nary_rules [] lem.proof in
-   let rules = List.flatten (List.map f lemmas) in
--  let rules1 = Misc.list_sort_unique Pervasives.compare rules in
-+  let rules1 = Misc.list_sort_unique Stdlib.compare rules in
-   let f r =
-     match r with
-     | Nary_case (n, oth) -> Isar_case.print_case "have" n oth oc

zenon.rpmlintrc

@@ -1,8 +0,0 @@
-# THIS FILE IS FOR WHITELISTING RPMLINT ERRORS AND WARNINGS IN TASKOTRON
-# https://fedoraproject.org/wiki/Taskotron/Tasks/dist.rpmlint#Whitelisting_errors
-
-# The dictionary is missing some technical terms
-addFilter(r'W: spelling-error .* prover')
-
-# The configure script is not an autotools-generated script
-addFilter(r'zenon\.spec:[^:]*: W: configure-without-libdir-spec')

zenon.spec

@@ -1,47 +1,46 @@
-%ifnarch %{ocaml_native_compiler}
 %global debug_package %{nil}
-%endif
-%global coqver 8.13.0
+%global rocqver 9.2.0
+%global giturl  https://github.com/zenon-prover/zenon
 
 Name:		zenon
-Version:	0.8.4
-Release:	21%{?dist}
+Version:	0.8.5
+Release:	43%{?dist}
 Summary:	Automated theorem prover for first-order classical logic
-License:	BSD
+License:	BSD-3-Clause
 URL:		http://zenon-prover.org/
-Source0:	https://github.com/zenon-prover/%{name}/archive/%{version}/%{name}-%{version}.tar.gz
+VCS:		git:%{giturl}.git
+Source0:	%{giturl}/archive/%{version}/%{name}-%{version}.tar.gz
 Source1:	http://zenon-prover.org/zenlpar07.pdf
 Source2:	%{name}-tptp-COM003+2.p
 Source3:	%{name}-tptp-ReadMe
 # Basic documentation (man pages). Submitted upstream 2008-07-25:
 Source4:	%{name}.1
 Source5:	%{name}-format.5
-# Adapt to coq 8.9
-Patch0:		%{name}-coq89.patch
-# Adapt to ocaml 4.08 and later
-Patch1:		%{name}-ocaml.patch
+# Update deprecated usage
+Patch:          %{name}-deprecated.patch
 
-# https://bugzilla.redhat.com/show_bug.cgi?id=1874879
-ExcludeArch: s390x
+# Rocq's plugin architecture requires cmxs files
+ExclusiveArch:  %{ocaml_native_compiler}
 
-BuildRequires:	coq = %{coqver}
-BuildRequires:	ghostscript-core
-BuildRequires:	ImageMagick
+BuildRequires:	coq-core-compat = %{rocqver}
+BuildRequires:	rocq = %{rocqver}
+BuildRequires:	rocq-stdlib
 BuildRequires:	make
 BuildRequires:	ocaml
 
-Requires:	coq%{?_isa} = %{coqver}
+Requires:	rocq%{?_isa} = %{rocqver}
+Requires:	rocq-stdlib%{?_isa}
 Requires:	coreutils
 
 %description
-Zenon is an automated theorem prover for first order classical logic
-with equality, based on the tableau method.  Zenon can read input files
-in TPTP, Coq, Focal, and its own Zenon format.  Zenon can directly
-generate Coq proofs (proof scripts or proof terms), which can be
-reinserted into Coq specifications.  Zenon can also be extended.
+Zenon is an automated theorem prover for first order classical logic with
+equality, based on the tableau method.  Zenon can read input files in TPTP,
+Coq, Focal, and its own Zenon format.  Zenon can directly generate Coq proofs
+(proof scripts or proof terms), which can be reinserted into Coq
+specifications.  Zenon can also be extended.
 
 %prep
-%autosetup -p0
+%autosetup -p1
 
 cp -p %{SOURCE1} .
 
@@ -55,14 +54,8 @@ mkdir examples
 cp -p %{SOURCE2} examples/tptp-COM003+2.p
 cp -p %{SOURCE3} examples/tptp-ReadMe
 
-# Work around Makefile errors (fails if no ocamlopt, uses _bytecode_ otherwise)
-%ifarch %{ocaml_native_compiler}
-  make %{?_smp_mflags} zenon.bin
-  cp -p zenon.bin zenon
-%else
-  make %{?_smp_mflags} zenon.byt
-  cp -p zenon.byt zenon
-%endif
+make %{?_smp_mflags} zenon.bin
+cp -p zenon.bin zenon
 # Use of %%{?_smp_mflags} sometimes leads to build failures
 make coq
 
@@ -95,10 +88,162 @@ fi
 %license LICENSE
 %{_bindir}/%{name}
 %{_libdir}/coq/user-contrib/Zenon
-%{_mandir}/man1/*
-%{_mandir}/man5/*
+%{_mandir}/man1/zenon.1*
+%{_mandir}/man5/zenon-format.5*
 
 %changelog
+* Wed Jul 29 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-43
+- Rebuild to fix rocq dependencies
+
+* Fri Jul 17 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-42
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild
+
+* Thu Jul 09 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-41
+- OCaml 5.5.0 rebuild
+
+* Thu Apr 16 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-40
+- Rebuild for rocq 9.2.0
+
+* Thu Mar 19 2026 Jerry James <loganjerry@gmail.com> - 0.8.5-39
+- Rebuild for rocq 9.1.1
+
+* Fri Feb 20 2026 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-38
+- OCaml 5.4.1 rebuild
+
+* Sat Jan 17 2026 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-37
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_44_Mass_Rebuild
+
+* Tue Oct 14 2025 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-36
+- OCaml 5.4.0 rebuild
+
+* Fri Aug 22 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-35
+- Bump and rebuild
+
+* Sun Aug 10 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-34
+- Bump and rebuild
+
+* Fri Jul 25 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-33
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_43_Mass_Rebuild
+
+* Sat Jul 12 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-32
+- Rebuild to fix OCaml dependencies
+
+* Wed Jan 22 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-31
+- Rebuild for coq 8.20.1
+
+* Sun Jan 19 2025 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-30
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_42_Mass_Rebuild
+
+* Fri Jan 10 2025 Jerry James <loganjerry@gmail.com> - 0.8.5-29
+- OCaml 5.3.0 rebuild for Fedora 42
+
+* Sat Jul 20 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-28
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_41_Mass_Rebuild
+
+* Wed Jun 19 2024 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-27
+- OCaml 5.2.0 ppc64le fix
+
+* Wed May 29 2024 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-26
+- OCaml 5.2.0 for Fedora 41
+
+* Fri Feb  2 2024 Jerry James <loganjerry@gmail.com> - 0.8.5-25
+- Rebuild for rebuilt coq
+
+* Sat Jan 27 2024 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-24
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
+* Tue Jan  2 2024 Jerry James <loganjerry@gmail.com> - 0.8.5-23
+- Rebuild for coq 8.18.0
+
+* Mon Dec 18 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-22
+- OCaml 5.1.1 + s390x code gen fix for Fedora 40
+
+* Tue Dec 12 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-21
+- OCaml 5.1.1 rebuild for Fedora 40
+
+* Thu Oct 05 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-20
+- OCaml 5.1 rebuild for Fedora 40
+
+* Thu Jul 27 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-19
+- Rebuild for ocaml-zarith 1.13
+
+* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-18
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
+
+* Wed Jul 12 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-17
+- OCaml 5.0 rebuild for Fedora 39
+
+* Mon Jul 10 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-16
+- OCaml 5.0.0 rebuild
+
+* Sat Apr  1 2023 Jerry James <loganjerry@gmail.com> - 0.8.5-15
+- Rebuild for coq 8.17.0
+
+* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-14
+- Bump release and rebuild
+
+* Tue Jan 24 2023 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-13
+- Rebuild OCaml packages for F38
+
+* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-12
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
+
+* Sat Nov 26 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-11
+- Rebuild for coq 8.16.1
+
+* Fri Sep 16 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-10
+- Rebuild for coq 8.16.0
+
+* Thu Aug 18 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-9
+- Rebuild to fix coq dependency
+- Convert License tag to SPDX
+
+* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-8
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
+
+* Wed Jul 20 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-7
+- Remove i686 support
+
+* Sun Jun 19 2022 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-7
+- OCaml 4.14.0 rebuild
+
+* Fri Mar 25 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-6
+- Rebuild for coq 8.15.1
+
+* Mon Feb 28 2022 Jerry James <loganjerry@gmail.com> - 0.8.5-5
+- Rebuild for coq 8.15.0
+
+* Fri Feb 04 2022 Richard W.M. Jones <rjones@redhat.com> - 0.8.5-4
+- OCaml 4.13.1 rebuild to remove package notes
+
+* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.5-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
+
+* Tue Nov 30 2021 Jerry James <loganjerry@gmail.com> - 0.8.5-2
+- Rebuild for coq 8.14.1
+
+* Thu Oct 21 2021 Jerry James <loganjerry@gmail.com> - 0.8.5-1
+- Version 0.8.5
+- Drop upstreamed -coq89 and -ocaml patches
+
+* Tue Oct 05 2021 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-27
+- OCaml 4.13.1 build
+
+* Mon Oct 04 2021 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-26
+- Try to build on s390x with OCaml 4.13
+
+* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 0.8.4-25
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
+
+* Tue Jun  8 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-24
+- Rebuild for coq 8.13.2
+
+* Wed Mar  3 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-23
+- Rebuild for coq 8.13.1
+
+* Tue Mar  2 11:03:37 GMT 2021 Richard W.M. Jones <rjones@redhat.com> - 0.8.4-22
+- OCaml 4.12.0 build
+
 * Sat Feb 20 2021 Jerry James <loganjerry@gmail.com> - 0.8.4-21
 - Rebuild for coq 8.13.0